instCompactlyGeneratedSpaceSigma — Mathlib

English

The sigma-type of a family of compactly generated spaces is compactly generated.

Русский

Сигма-тип семейства компактно-генерируемых пространств является компактно-генерируемым.

LaTeX

$$$\\text{CompactlyGeneratedSpace}(\\Sigma i, X_i)$$$

Lean4

/-- The sigma type associated to a family of compactly generated spaces is compactly generated. -/
instance {ι : Type u} {X : ι → Type v} [∀ i, TopologicalSpace (X i)] [∀ i, CompactlyGeneratedSpace (X i)] :
    CompactlyGeneratedSpace (Σ i, X i) :=
  by
  refine
    compactlyGeneratedSpace_of_isClosed fun s h ↦
      isClosed_sigma_iff.2 fun i ↦ CompactlyGeneratedSpace.isClosed' fun K _ _ _ f hf ↦ ?_
  let g : ULift.{u} K → (Σ i, X i) := Sigma.mk i ∘ f ∘ ULift.down
  have hg : Continuous g := continuous_sigmaMk.comp <| hf.comp continuous_uliftDown
  exact (h _ g hg).preimage continuous_uliftUp

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