discreteTopology — Mathlib

English

If each Y i has a discrete topology, then the Sigma-type Σ Y has a discrete topology.

Русский

Если каждый Y i дискретен, то Sigma-обобщение Σ Y дискретно.

LaTeX

$$$ [\\forall i, TopologicalSpace (Y i)] [\\forall i, DiscreteTopology (Y i)] :\\; \\text{DiscreteTopology}(\\Sigma Y). $$$

Lean4

instance discreteTopology {ι : Type*} {Y : ι → Type v} [∀ i, TopologicalSpace (Y i)] [h : ∀ i, DiscreteTopology (Y i)] :
    DiscreteTopology (Sigma Y) :=
  ⟨iSup_eq_bot.2 fun _ => by simp only [(h _).eq_bot, coinduced_bot]⟩

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