le_map_cofinite — Mathlib

English

If f is surjective, then cofinite ≤ map f cofinite; i.e., pushing forward cofinite by a surjective map preserves cofinite-ness.

Русский

Если f сюръективна, то кофинитный фильтр не уменьшается при отображении через f: cofinite ≤ map f cofinite.

LaTeX

$$$\\text{Surjective}(f) \\Rightarrow \\operatorname{cofinite} \\le \\operatorname{map} f (\\operatorname{cofinite})$$$

Lean4

theorem le_map_cofinite {f : α → β} (hf : Surjective f) : cofinite ≤ map f cofinite := fun _ h => .of_preimage h hf

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