instDiscreteTopologyMultiplicative

English

If X has the discrete topology, then the multiplicative version Multiplicative X also has the discrete topology.

Русский

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

LaTeX

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

Lean4

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

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