comap_cofinite_eq — Mathlib

English

For an injective map f, comap f cofinite equals cofinite.

Русский

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

LaTeX

$$$\\operatorname{comap}_f(\\operatorname{cofinite}) = \\operatorname{cofinite}$$$

Lean4

/-- The pullback of the `Filter.cofinite` under an injective function is equal to `Filter.cofinite`.
See also `Filter.comap_cofinite_le` and `Function.Injective.tendsto_cofinite`. -/
theorem comap_cofinite_eq {f : α → β} (hf : Injective f) : comap f cofinite = cofinite :=
  (comap_cofinite_le f).antisymm hf.tendsto_cofinite.le_comap

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