instDiscreteTopologyProd — Mathlib

English

If X and Y have discrete topology, then X × Y also has the discrete topology.

Русский

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

LaTeX

$$$\\text{DiscreteTopology}(X) \\land \\text{DiscreteTopology}(Y) \\Rightarrow \\text{DiscreteTopology}(X \\times Y)$$$

Lean4

instance [DiscreteTopology X] [DiscreteTopology Y] : DiscreteTopology (X × Y) :=
  discreteTopology_iff_nhds.2 fun (a, b) => by rw [nhds_prod_eq, nhds_discrete X, nhds_discrete Y, prod_pure_pure]

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