[isabelle] mono_on and strict_mono_on
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] mono_on and strict_mono_on
- From: Manuel Eberl <eberlm at in.tum.de>
- Date: Wed, 25 Jun 2014 03:58:46 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.5.0
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and