Ici_le_id — Mathlib

English

If φ is strictly monotone on Ici n, then for all m with n ≤ m, φ(m) ≤ m.

Русский

Если φ строго монотонна на Ici n, то для всех m с n ≤ m верно φ(m) ≤ m.

LaTeX

$$$\forall m, n \le m \Rightarrow φ(m) \le m.$$$

Lean4

theorem Ici_le_id [PredOrder α] [IsPredArchimedean α] [OrderTop α] {n : α} {φ : α → α}
    (hφ : StrictMonoOn φ (Set.Ici n)) : ∀ m, n ≤ m → φ m ≤ m :=
  StrictMonoOn.Iic_id_le (α := αᵒᵈ) fun _ hi _ hj hij => hφ hj hi hij

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