cofinite_of_finite_preimage_singleton

English

For a function with finite preimages of singletons, Tendsto f cofinite cofinite holds.

Русский

Для функции, у которой прообраз каждой единичной пары конечен, выполняется сходимость к кофинитному фильтру.

LaTeX

$$$\\forall b, \\text{Finite}(f^{-1}({b})) \\Rightarrow \\operatorname{Tendsto} f (\\operatorname{cofinite}) (\\operatorname{cofinite})$$$

Lean4

/-- For a function with finite fibres, inverse images of finite sets are finite. -/
theorem cofinite_of_finite_preimage_singleton {f : α → β} (hf : ∀ b, Finite (f ⁻¹' { b })) :
    Tendsto f cofinite cofinite := fun _ h => h.preimage' fun b _ ↦ hf b

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