Theorems · Theorem · order theory

strictMono_iff_map_pos

∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F)
  [iamhc : AddMonoidHomClass F α β], StrictMono ⇑f ↔ ∀ (a : α), 0 < a → 0 < f a

Defined in

Mathlib.Algebra.Order.Hom.Monoid

Cited by

3 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupPartialOrderIsOrderedAddMonoidAddCommGroupPartialOrderIsOrderedAddMonoidFunLikeAddMonoidHomClass