univ — Mathlib

English

The universal set of X is homeomorphic to X itself.

Русский

Универсальное множество X гомеоморфно самому X.

LaTeX

$$$ (\mathrm{univ} : Set X) \cong_{Top} X. $$$

Lean4

/-- `Set.univ X` is homeomorphic to `X`. -/
@[simps! -fullyApplied]
def univ (X : Type*) [TopologicalSpace X] : (univ : Set X) ≃ₜ X
    where
  toEquiv := Equiv.Set.univ X
  continuous_toFun := continuous_subtype_val
  continuous_invFun := continuous_id.subtype_mk _

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