Email Gateway (Aug 19 2022 at 14:38): Email Gateway (Aug 19 2022 at 14:38):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I recently found myself in a situation where it would have been useful
to have something like mono_on and strict_mono on, i.e.
mono_on f A = (∀x y. x ∈ A ∧ y ∈ A ∧ x ≤ y ⟶ f x ≤ f y
strict_mono_on f A = (∀x y. x ∈ A ∧ y ∈ A ∧ x < y ⟶ f x < f y
Seeing as e.g. inj_on is in HOL, I would argue it makes sense to include
these definitions as well. Would it be possible to put them in?
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 14:38):From: Tobias Nipkow <nipkow@in.tum.de>
I don't like to put things in proactively. Mark them as to be moved, and once
your development goes into the AFP (for example), we can consider globalizing them.
Tobias
Last updated: Nov 21 2024 at 12:39 UTC