Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] strict_mono with an explicit set

view this post on Zulip 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

view this post on Zulip 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: Nov 21 2024 at 12:39 UTC