Email Gateway (Aug 23 2022 at 08:19): Email Gateway (Aug 23 2022 at 08:19):From: Lawrence Paulson <lp15@cam.ac.uk>
We have the monotonicity predicate strict_mono. But do we have its obvious generalisation?
definition strict_mono_on :: "('a ⇒ 'b::order)⇒ 'a set ⇒ bool” where
"strict_mono_on f A ⟷ (∀x y. x < y ∧ x ∈ A ∧ y ∈ A ⟶ f x < f y)”
Larry Paulson
Email Gateway (Aug 23 2022 at 08:19):From: Manuel Eberl <eberlm@in.tum.de>
Apparently we do, in src/HOL/Analysis/Borel_Space.thy.
Don't ask me why. Yes, it should be moved.
Manuel
Last updated: Apr 20 2024 at 08:16 UTC