strictMono_iff_map_pos — Mathlib

English

Let f: α → β be a map between ordered additive groups. Then f is strictly monotone if and only if 0 < a implies 0 < f(a) for all a.

Русский

Пусть f: α → β — отображение между упорядоченными дополнительными группами. Тогда f строго монотонна тогда и только тогда, когда для каждого a выполняется 0 < a ⇒ 0 < f(a).

LaTeX

$$$StrictMono(f) \\iff \\forall a,\\; 0 < a \\rightarrow 0 < f(a)$$$

Lean4

theorem strictMono_iff_map_pos : StrictMono (f : α → β) ↔ ∀ a, 0 < a → 0 < f a :=
  by
  refine ⟨fun h a => ?_, fun h a b hl => ?_⟩
  · rw [← map_zero f]
    apply h
  · rw [← sub_add_cancel b a, map_add f]
    exact lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)

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