of_le_map_sup — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem of_le_map_sup [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : ∀ x y, f x ⊔ f y ≤ f (x ⊔ y)) :
    Monotone f :=
  monotone_dual_iff.mp <| of_map_inf_le h

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