map_sup_le — Mathlib

English

If f is antitone and α, β have sup, then f(x ⊔ y) ≤ f x ⊔ f y.

Русский

Если f антитонная и есть операция верхнего объединения, то f(x ⊔ y) ≤ f(x) ⊔ f(y).

LaTeX

$$$ [SemilatticeSup \alpha] [SemilatticeInf \beta] {f : \alpha → β} (h : Antitone f) (x y : \alpha) : f(x \sqcup y) ≤ f(x) \wedge f(y)$$$

Lean4

theorem map_sup_le [SemilatticeSup α] [SemilatticeInf β] {f : α → β} (h : Antitone f) (x y : α) :
    f (x ⊔ y) ≤ f x ⊓ f y :=
  h.dual_right.le_map_sup x y

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