eq_compactlyGenerated — Mathlib

English

For X with a topology t and if X is UCompactlyGeneratedSpace, then t equals the compactlyGenerated topology (alternative formulation).

Русский

Для X с топологией t и если X — UCompactlyGeneratedSpace, то t равно компактно-генерируемой топологии (альтернативное формулирование).

LaTeX

$$$ [t : TopologicalSpace X] [UCompactlyGeneratedSpace X] \Rightarrow t = \operatorname{compactlyGenerated}(X) $$$

Lean4

theorem eq_compactlyGenerated [t : TopologicalSpace X] [UCompactlyGeneratedSpace.{u} X] :
    t = compactlyGenerated.{u} X := by
  apply le_antisymm
  · exact UCompactlyGeneratedSpace.le_compactlyGenerated
  · simp only [compactlyGenerated, ← continuous_iff_coinduced_le, continuous_sigma_iff, Sigma.forall]
    exact fun S f ↦ f.2

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