Theorems · Theorem · group theory

AddConstMapClass.strictMono_iff_Icc

∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommGroup G]
  [inst_2 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [inst_5 : AddCommGroup H] [inst_6 : PartialOrder H]
  [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F},
  0 < a → ∀ (l : G), StrictMono ⇑f ↔ StrictMonoOn (⇑f) (Set.Icc l (l + a))

Defined in

Mathlib.Algebra.AddConstMap.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FunLikeAddCommGroupLinearOrderIsOrderedAddMonoidArchimedeanAddCommGroupPartialOrderIsOrderedAddMonoidAddConstMapClass