instDiscreteTopologyAdditive — Mathlib

English

If X has the discrete topology, then the additive version Additive X also has the discrete topology.

Русский

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

LaTeX

$$$\operatorname{DiscreteTopology}(X) \implies \operatorname{DiscreteTopology}(\mathrm{Additive}\,X)$$$

Lean4

instance [DiscreteTopology X] : DiscreteTopology (Additive X) :=
  ‹DiscreteTopology X›

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