tendsto_finset_preimage_atTop_atTop

English

Same as previous: preimage operation preserves Tendsto to atTop under injectivity.

Русский

То же самое: операция предобраза сохраняет Tendsto к atTop при инъективности.

LaTeX

$$$\operatorname{Tendsto}(s \mapsto s^{-1} \!\!\!_f, \operatorname{atTop}, \operatorname{atTop})$$$

Lean4

theorem tendsto_finset_preimage_atTop_atTop {f : α → β} (hf : Function.Injective f) :
    Tendsto (fun s : Finset β => s.preimage f (hf.injOn)) atTop atTop :=
  (Finset.monotone_preimage hf).tendsto_atTop_finset fun x =>
    ⟨{f x}, Finset.mem_preimage.2 <| Finset.mem_singleton_self _⟩

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