iSup — Mathlib

English

Suprema of delta-generated topologies are delta-generated.

Русский

Супримы дельта-генерируемых топологий также дельта-генерируемые.

LaTeX

$$$$\text{DeltaGeneratedSpace}(X, \bigsqcup_i t_i) \text{ when each } \text{DeltaGeneratedSpace}(X, t_i).$$$$

Lean4

/-- Suprema of delta-generated topologies are delta-generated. -/
protected theorem iSup {X : Type*} {ι : Sort*} {t : ι → TopologicalSpace X} (h : ∀ i, @DeltaGeneratedSpace X (t i)) :
    @DeltaGeneratedSpace X (⨆ i, t i) :=
  let _ := ⨆ i, t i
  ⟨iSup_le_iff.2 fun i ↦ (h i).le_deltaGenerated.trans <| deltaGenerated_mono <| le_iSup t i⟩

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