coe_sup — Mathlib

English

The embedding of the interval Icc(a,b) into α preserves suprema as well: the image of x ⊔ y equals the supremum of the images, i.e., ↑(x ⊔ y) = ↑x ⊔ ↑y.

Русский

Пусть Icc(a,b) вложен в α; верхняя граница сохраняется: образ x ⊔ y равен sup образов x и y.

LaTeX

$$$\uparrow(x \lor y) = (\uparrow x) \lor (\uparrow y).$$$

Lean4

@[simp, norm_cast]
protected theorem coe_sup [SemilatticeSup α] {x y : Icc a b} : ↑(x ⊔ y) = (↑x ⊔ ↑y : α) :=
  rfl

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