instFirstCountableTopologyForallOfCountable

English

In a product of countably many spaces, if each factor is first-countable, then the product is first-countable.

Русский

В произведении счётного числа пространств, если каждая фактор имеет первую счётность, то произведение также первая счётна.

LaTeX

$$$\text{FirstCountableTopology}(\forall i, X_i)$$$

Lean4

instance {ι : Type*} {X : ι → Type*} [Countable ι] [∀ i, TopologicalSpace (X i)] [∀ i, FirstCountableTopology (X i)] :
    FirstCountableTopology (∀ i, X i) :=
  ⟨fun f => by rw [nhds_pi]; infer_instance⟩

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