map_inf — Mathlib

English

Let α be a linear order and β a semilattice with join. If f: α → β is antitone, then for all x, y ∈ α, f(x ∧ y) = f(x) ∨ f(y).

Русский

Пусть α — линейно упорядоченное множество, β — полузамкнутая по операции ⊔. Пусть f: α → β антимотонна. Тогда для любых x, y ∈ α выполняется f(x ∧ y) = f(x) ∨ f(y).

LaTeX

$$$\forall x\in\alpha\,\forall y\in\alpha:\ f(x\wedge y)=f(x)\vee f(y)$$$

Lean4

theorem map_inf [SemilatticeSup β] {f : α → β} (hf : Antitone f) (x y : α) : f (x ⊓ y) = f x ⊔ f y :=
  hf.dual_right.map_inf x y

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