countable_mulSupport — Mathlib

English

In a FirstCountable and T1 topological group, if f is Multipliable, then its mulSupport is countable.

Русский

В топологической группе первого счета и T1, если f — Multipliable, то его mulSupport счётно.

LaTeX

$$$$ (f.mulSupport).Countable $$$$

Lean4

@[to_additive]
theorem countable_mulSupport [FirstCountableTopology G] [T1Space G] (hf : Multipliable f) : f.mulSupport.Countable := by
  simpa only [ker_nhds] using hf.tendsto_cofinite_one.countable_compl_preimage_ker

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