le_map_sup — Mathlib

English

Let α and β be semilattices with supremum and f: α → β a monotone function. Then for all x, y ∈ α, f(x) ⊔ f(y) ≤ f(x ⊔ y).

Русский

Пусть α и β — полусуп-решётки, причём f: α → β монотонна. Тогда для любых x, y ∈ α выполняется f(x) ⊔ f(y) ≤ f(x ⊔ y).

LaTeX

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

Lean4

theorem le_map_sup [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : Monotone f) (x y : α) :
    f x ⊔ f y ≤ f (x ⊔ y) :=
  sup_le (h le_sup_left) (h le_sup_right)

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