instFirstCountableTopology — Mathlib

English

If G is FirstCountable, then the quotient G/N is also FirstCountable.

Русский

Если G имеет свойство первой счётности, то и G/N имеет это свойство.

LaTeX

$$[FirstCountableTopology G] ⇒ FirstCountableTopology (G ⧸ N).$$

Lean4

@[to_additive]
instance instFirstCountableTopology [FirstCountableTopology G] : FirstCountableTopology (G ⧸ N) where
  nhds_generated_countable := mk_surjective.forall.2 fun x ↦ nhds_eq N x ▸ inferInstance

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