inclusionTopIso — Mathlib

English

The top open subset of X, which is the whole space, is canonically isomorphic to X in TopCat.

Русский

Общее открытое множество ⊤ в X канонически изоморфно X в категории TopCat.

LaTeX

$$$(\\text{toTopCat }X)\\_{}.\\text{obj } \\top \\cong X$$$

Lean4

/-- The inclusion of the top open subset (i.e. the whole space) is an isomorphism.
-/
def inclusionTopIso (X : TopCat.{u}) : (toTopCat X).obj ⊤ ≅ X
    where
  hom := inclusion' ⊤
  inv := TopCat.ofHom ⟨fun x => ⟨x, trivial⟩, continuous_def.2 fun _ ⟨_, hS, hSU⟩ => hSU ▸ hS⟩

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