instFirstCountableTopology — Mathlib

English

If M has a first-countable topology, then the DomMulAct space Mᵈᵐᵃ also has a first-countable topology.

Русский

Если у M топология с базой окрестностей счётного типа, то у DomMulAct M такая же база.

LaTeX

$$$$ \operatorname{FirstCountableTopology}(M) \Rightarrow \operatorname{FirstCountableTopology}(\mathrm{DomMulAct}(M)) $$$$

Lean4

@[to_additive]
instance instFirstCountableTopology [FirstCountableTopology M] : FirstCountableTopology Mᵈᵐᵃ :=
  isInducing_mk_symm.firstCountableTopology

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