coe_sup — Mathlib

English

For any α and compact subsets s,t ⊆ α, the carrier of their join equals the union of their carriers: ↑(s ⊔ t) = ↑s ∪ ↑t.

Русский

Для любых компактных подмножеств s,t ⊆ α верна равенство носителей их объединения: \\uparrow(s \\sqcup t) = \\uparrow s \\cup \\uparrow t.

LaTeX

$$$\\forall \\alpha [\\text{TopologicalSpace }\\alpha] (s,t : \\mathrm{Compacts}(\\alpha)),\\quad \\uparrow (s \\sqcup t) = \\uparrow s \\cup \\uparrow t$$$

Lean4

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

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