mono — Mathlib

English

If f is left order continuous, then for every n, f^[n] is left order continuous.

Русский

Если f слева непрерывна, то для любого n отображение f^[n] тоже слева непрерывно.

LaTeX

$$$\text{LeftOrdContinuous}(f) \Rightarrow \forall n:\mathbb{N},\ \text{LeftOrdContinuous}(f^{[n]})$$$

Lean4

theorem mono (hf : LeftOrdContinuous f) : Monotone f := fun a₁ a₂ h =>
  have : IsGreatest { a₁, a₂ } a₂ := ⟨Or.inr rfl, by simp [*]⟩
  (hf.map_isGreatest this).2 <| mem_image_of_mem _ (Or.inl rfl)

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