coe_sup_interval — Mathlib

English

The sup of two nonempty intervals corresponds to the sup of their underlying sets.

Русский

Объединение (верхняя граница) двух непустых интервалов соответствует объединению их множеств.

LaTeX

$$$$ ↑(s \\sqcup t) = ↑s \\sqcup ↑t. $$$$

Lean4

@[simp, norm_cast]
theorem coe_sup_interval [Lattice α] (s t : NonemptyInterval α) : (↑(s ⊔ t) : Interval α) = ↑s ⊔ ↑t :=
  rfl

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