tendsto_of_forall_preimage — Mathlib

English

If a function f sends compact sets to compact preimages for every compact s ⊆ β, then f is Tendsto from cocompact α to cocompact β.

Русский

Если для каждого компактного s ⊆ β выполняется, что f^{-1}(s) компактно, то f является пределом Tendsto между cocompact α и cocompact β.

LaTeX

$$$(\\forall s, IsCompact s → IsCompact (f^{-1}(s))) \\implies Tendsto f (cocompact\\; α) (cocompact\\; β)$$

Lean4

theorem tendsto_of_forall_preimage {f : α → β} (h : ∀ s, IsCompact s → IsCompact (f ⁻¹' s)) :
    Tendsto f (cocompact α) (cocompact β) := fun s hs =>
  match mem_cocompact.mp hs with
  | ⟨t, ht, hts⟩ => mem_map.mpr (mem_cocompact.mpr ⟨f ⁻¹' t, h t ht, by simpa using preimage_mono hts⟩)

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