tendsto_norm_atTop_iff_cobounded'

English

For any f: α → E, Tendsto (∥f∥) l atTop is equivalent to Tendsto f l (cobounded E).

Русский

Для любого f: α → E, стремление ∥f∥ к бесконечности эквивалентно стремлению f к cobounded E.

LaTeX

$$Tendsto (\\|f\\|) l atTop ↔ Tendsto f l (cobounded E)$$

Lean4

@[to_additive (attr := simp) tendsto_norm_atTop_iff_cobounded]
theorem tendsto_norm_atTop_iff_cobounded' {f : α → E} {l : Filter α} :
    Tendsto (‖f ·‖) l atTop ↔ Tendsto f l (cobounded E) := by rw [← comap_norm_atTop', tendsto_comap_iff]; rfl

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