toCocompactMapClass_of_norm — Mathlib

English

If for all f in 𝓕 and all ε > 0 there exists r > 0 with ∀ x, r < ∥x∥ → ε < ∥f(x)∥, then 𝓕 forms a cocompact map class.

Русский

Если для каждого f из 𝓕 и для любого ε > 0 существует r > 0 с условием ∀ x, r < ∥x∥ → ε < ∥f(x)∥, то 𝓕 образует кококомпактный класс отображений.

LaTeX

$$$\forall (f:𝓕)(\forall \varepsilon>0),\ Exists r>0,\forall x, r<\|x\| \Rightarrow \varepsilon<\|f(x)\| \Rightarrow 𝓕\text{ является кококомпактным классом}$$$

Lean4

theorem toCocompactMapClass_of_norm [ProperSpace E] [FunLike 𝓕 E F] [ContinuousMapClass 𝓕 E F]
    (h : ∀ (f : 𝓕) (ε : ℝ), ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖) : CocompactMapClass 𝓕 E F where
  cocompact_tendsto := (tendsto_cocompact_cocompact_of_norm <| h ·)

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