coe_top — Mathlib

English

The top element ⊤ of NonemptyCompacts α corresponds to the whole space, i.e., its underlying set is univ.

Русский

Наивысший элемент ⊤ в NonemptyCompacts α соответствует всей области пространства: его носитель равен единице пространства.

LaTeX

$$$ (\uparrow(\top : \mathrm{NonemptyCompacts}\, \alpha) : \mathrm{Set}\,\alpha) = \mathrm{univ} $$$

Lean4

@[simp]
theorem coe_top [CompactSpace α] [Nonempty α] : (↑(⊤ : NonemptyCompacts α) : Set α) = univ :=
  rfl

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