instAlexandrovDiscrete — Mathlib

English

Let X and Y be topological spaces with Alexandrov-discrete topology. Then their Cartesian product X × Y also has Alexandrov-discrete topology.

Русский

Пусть X и Y — топологические пространства с Александровской дискретной топологией. Тогда декартово произведение X × Y тоже имеет Александрову дискретную топологию.

LaTeX

$$$AlexandrovDiscrete(\alpha) \land AlexandrovDiscrete(\beta) \to AlexandrovDiscrete(\alpha \times \beta)$$$

Lean4

instance instAlexandrovDiscrete : AlexandrovDiscrete (α × β) := by
  simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
    prod_principal_principal, nhdsKer_pair, forall_true_iff]

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