strictMono_symm — Mathlib

English

If an equals-structure map e is strictly monotone, then its inverse e.symm is also strictly monotone.

Русский

Если отображение e строго монотонно, то и его обратное e.symm строго монотонно.

LaTeX

$$StrictMono e → StrictMono e.symm$$

Lean4

@[to_additive]
theorem strictMono_symm {G G' : Type*} [CommMonoid G] [LinearOrder G] [CommMonoid G'] [PartialOrder G'] {e : G ≃* G'}
    (he : StrictMono e) : StrictMono e.symm := by
  intro
  simp [← he.lt_iff_lt]

Похожие утверждения