coe_sup — Mathlib

English

Let X be a topological space and s,t be open subsets of X. Then the underlying set of their join equals the union of their underlying sets.

Русский

Пусть X — топологическое пространство и s,t — открытые подмножества X. Тогда множество, соответствующее их объединению как открытого множества, равно объединению множеств s и t.

LaTeX

$$$ (\uparrow (s \sqcup t) : Set \alpha) = (\uparrow s) \cup (\uparrow t) $$$

Lean4

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

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