countable_compl_preimage_ker — Mathlib

English

If f tends to a countably generated filter l along cofinites, then the complement of the preimage of l.ker is countable.

Русский

Если функция f стремится к счётному сгенерированному фильтру л along cofinite, тогда комплемент предобраза l.ker счётен.

LaTeX

$$∀ {f}, {l}, [l.IsCountablyGenerated] (Tendsto f cofinites l) → Countable((f^{-1} l.ker)^c)$$

Lean4

/-- If `f` tends to a countably generated filter `l` along `Filter.cofinite`,
then for all but countably many elements, `f x ∈ l.ker`. -/
theorem countable_compl_preimage_ker {f : α → β} {l : Filter β} [l.IsCountablyGenerated] (h : Tendsto f cofinite l) :
    Set.Countable (f ⁻¹' l.ker)ᶜ := by rw [← ker_comap]; exact countable_compl_ker h.le_comap

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