instUCompactlyGeneratedSpaceSigma

English

The sigma type Σ i, X_i is compactly generated if every X_i is compactly generated.

Русский

Если каждый X_i компактно-генерируемый, то Σ i, X_i компактно-генерируемый.

LaTeX

$$$ \forall i, \operatorname{TopologicalSpace}(X_i) \wedge \forall i, \operatorname{UCompactlyGeneratedSpace}(X_i) \Rightarrow \operatorname{UCompactlyGeneratedSpace}(\Sigma i, X_i) $$$

Lean4

/-- The sigma type associated to a family of compactly generated spaces is compactly generated. -/
instance {ι : Type v} {X : ι → Type w} [∀ i, TopologicalSpace (X i)] [∀ i, UCompactlyGeneratedSpace.{u} (X i)] :
    UCompactlyGeneratedSpace.{u} (Σ i, X i) :=
  uCompactlyGeneratedSpace_of_isClosed fun _ h ↦
    isClosed_sigma_iff.2 fun i ↦
      UCompactlyGeneratedSpace.isClosed fun S ⟨f, hf⟩ ↦ h S ⟨Sigma.mk i ∘ f, continuous_sigmaMk.comp hf⟩

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