coe_sup — Mathlib

English

The inclusion (coercion) map from Complementeds α to α preserves sup: for any a,b in Complementeds α, the underlying element of their join equals the join of their underlying elements.

Русский

Включение из Complementeds α в α сохраняет сумму: для любых a,b ∈ Complementeds α основанные элементы их соединения равны объединению их оснований.

LaTeX

$$$\forall a,b\in \mathrm{Complementeds}(\alpha),\ \uparrow(a \lor b) = (a : \alpha) \lor (b : \alpha).$$$

Lean4

@[simp, norm_cast]
theorem coe_sup (a b : Complementeds α) : ↑(a ⊔ b) = (a : α) ⊔ b :=
  rfl

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