isCountablyGenerated — Mathlib

English

If l is countably generated, then comap f l is countably generated.

Русский

Если l счетно порожден, то comap f l счетно порожден.

LaTeX

$$$\\operatorname{IsCountablyGenerated}(l) \\rightarrow \\operatorname{IsCountablyGenerated}(\\mathrm{comap}~f~l)$$$

Lean4

instance isCountablyGenerated (l : Filter β) [l.IsCountablyGenerated] (f : α → β) : (comap f l).IsCountablyGenerated :=
  let ⟨_x, hxl⟩ := l.exists_antitone_basis
  (hxl.comap _).isCountablyGenerated

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