[isabelle] mono_on and strict_mono_on



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.