Re: [isabelle] mono_on and strict_mono_on
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.
On 25/06/2014 03:58, Manuel Eberl wrote:
> 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