coe_sup

Mathlib.Topology.Sets.Compacts

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.NonemptyCompacts.coe_sup

English

The underlying set of the join of two nonempty compacts equals the union of their underlying sets.

Русский

Носитель объединения двух непустых компактных множеств равен объединению их носителей.

LaTeX

$$$ (K ⊔ L : \mathrm{Set}\,\alpha) = K \cup L $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru