map_sup — Mathlib

English

If f is left order continuous and α, β are semilattices with ⊔, then f(x ⊔ y) = f x ⊔ f y.

Русский

Если f слева непрерывна и ⊔ — операция объединения в полупорядоченном множестве, то f(x ⊔ y) = f(x) ⊔ f(y).

LaTeX

$$$\text{LeftOrdContinuous}(f) \rightarrow f(x \lor y) = f(x) \lor f(y)$$$

Lean4

theorem map_sup (hf : LeftOrdContinuous f) (x y : α) : f (x ⊔ y) = f x ⊔ f y :=
  (hf isLUB_pair).unique <| by simp only [image_pair, isLUB_pair]

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