of_left_le_map_sup — Mathlib

English

If f(x) ≤ f(x ⊔ y) for all x, y, then f is monotone.

Русский

Если для всех x, y выполняется f(x) ≤ f(x ⊔ y), то f монотонна.

LaTeX

$$$ [SemilatticeSup \alpha] [Preorder \beta] \{f : \alpha \to \beta\} (h : \forall x y, f(x) \le f(x \lor y)) \Rightarrow Monotone f$$$

Lean4

theorem of_left_le_map_sup [SemilatticeSup α] [Preorder β] {f : α → β} (h : ∀ x y, f x ≤ f (x ⊔ y)) : Monotone f :=
  monotone_dual_iff.1 <| of_map_inf_le_left h

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