tendsto_cofinite — Mathlib

English

For an injective function, the pullback of the cofinite filter equals cofinite.

Русский

Для инъективной функции прообраз кофинитного фильтра равен кофинитному фильтру.

LaTeX

$$$\\text{Injective}(f) \\Rightarrow \\operatorname{comap}_f(\\operatorname{cofinite}) = \\operatorname{cofinite}$$$

Lean4

/-- For an injective function `f`, inverse images of finite sets are finite. See also
`Filter.comap_cofinite_le` and `Function.Injective.comap_cofinite_eq`. -/
theorem tendsto_cofinite {f : α → β} (hf : Injective f) : Tendsto f cofinite cofinite := fun _ h => h.preimage hf.injOn

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