coe_eq_univ — Mathlib

English

A closed set has underlying set equal to the whole space if and only if that closed set is the top element.

Русский

Замкнутое множество имеет множество равное всему пространству тогда и только тогда, когда это множество равно верхнему элементу.

LaTeX

$$$(s : \mathrm{Closeds}(\alpha))\uparrow = \mathrm{univ} \iff s = \top.$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_univ {s : Closeds α} : (s : Set α) = univ ↔ s = ⊤ :=
  SetLike.coe_injective.eq_iff' rfl

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