le_map_inf — Mathlib

English

If f is antitone with α, β as described, then f x ⊔ f y ≤ f(x ⊓ y).

Русский

Если f антитонна, то f(x) ⊔ f(y) ≤ f(x ⊓ y).

LaTeX

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

Lean4

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

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