coe_sup — Mathlib

English

For any two closed sets s and t, the underlying set of their join equals the union of their underlying sets. In other words, the closed-set join corresponds to the set-theoretic union.

Русский

Для любых двух замкнутых множеств s и t множества, лежащие в их объединении, совпадают: множество-объект, порождаемый их наслоением, равняется объединению их множеств.

LaTeX

$$$\forall s,t \in \mathrm{Closeds}(\alpha):\ (s \lor t)^{\uparrow} = s^{\uparrow} \cup t^{\uparrow}.$$$

Lean4

@[simp, norm_cast]
theorem coe_sup (s t : Closeds α) : (↑(s ⊔ t) : Set α) = ↑s ∪ ↑t := by rfl

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