tendsto_cofinite_cocompact_iff — Mathlib

English

For any f: X → Y, Tendsto f cofinite (cocompact Y) holds if and only if the preimage of every compact subset K ⊆ Y is finite.

Русский

Для отображения f: X → Y верно: Tendsto f cofinite (cocompact Y) тогда и только тогда, когда прообраз любого компактного множества K ⊆ Y конечен.

LaTeX

$$$\\operatorname{Tendsto} f\\, \\operatorname{cofinite}\\ (\\operatorname{cocompact}\\ Y) \\iff \\forall K,\\ IsCompact(K) \\to (f^{-1}(K)) \\text{ finite}$$$

Lean4

theorem tendsto_cofinite_cocompact_iff : Tendsto f cofinite (cocompact _) ↔ ∀ K, IsCompact K → Set.Finite (f ⁻¹' K) :=
  by
  rw [hasBasis_cocompact.tendsto_right_iff]
  refine forall₂_congr (fun K _ ↦ ?_)
  simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]

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