instFirstCountableTopologyProd — Mathlib

English

In a product of two spaces with first-countable topologies, the product is first-countable

Русский

Произведение двух пространств с первой счётностью имеет первую счётность.

LaTeX

$$$\text{FirstCountableTopology}(\alpha \times \beta)$$$

Lean4

instance {β} [TopologicalSpace β] [FirstCountableTopology α] [FirstCountableTopology β] :
    FirstCountableTopology (α × β) :=
  ⟨fun ⟨x, y⟩ => by rw [nhds_prod_eq]; infer_instance⟩

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