instUCompactlyGeneratedSpaceCarrierToTopCat

English

For every condensed set X, the underlying topological space of its carrier X.toTopCat is a UCompactlyGeneratedSpace.

Русский

Для каждого конденсированного множества X связанная топологическая конфигурация X.toTopCat является пространством с характеристикой UCompactlyGenerated.

LaTeX

$$$\mathrm{UCompactlyGeneratedSpace}(X^{\mathrm{toTopCat}}.\mathrm{carrier})$$$

Lean4

instance (X : CondensedSet.{u}) : UCompactlyGeneratedSpace.{u, u + 1} X.toTopCat :=
  by
  apply uCompactlyGeneratedSpace_of_continuous_maps
  intro Y _ f h
  rw [continuous_coinduced_dom, continuous_sigma_iff]
  exact fun ⟨S, s⟩ ↦ h S ⟨_, continuous_coinducingCoprod X _⟩

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