discreteTopology — Mathlib

English

If X and Y are topological spaces with discrete topologies, then X ⊕ Y has a discrete topology.

Русский

Если X и Y имеют дискретные топологии, то сумма X ⊕ Y тоже дискретна.

LaTeX

$$$ [\\text{TopologicalSpace } X] [\\text{TopologicalSpace } Y] [\\text{DiscreteTopology } X] [\\text{DiscreteTopology } Y] :\\; \\text{DiscreteTopology}(X \\oplus Y). $$$

Lean4

instance discreteTopology [TopologicalSpace X] [TopologicalSpace Y] [h : DiscreteTopology X] [hY : DiscreteTopology Y] :
    DiscreteTopology (X ⊕ Y) :=
  ⟨sup_eq_bot_iff.2 <| by simp [h.eq_bot, hY.eq_bot]⟩

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