eventually_cobounded_le_norm' — Mathlib

English

For any real a, almost every x in cobounded E satisfies a ≤ ∥x∥.

Русский

Для каждого вещественного a почти во всех x в cobounded E выполняется a ≤ ∥x∥.

LaTeX

$$∀ a ∈ ℝ, ∀ᶠ x ∈ cobounded E, a ≤ ∥x∥$$

Lean4

@[to_additive eventually_cobounded_le_norm]
theorem eventually_cobounded_le_norm' (a : ℝ) : ∀ᶠ x in cobounded E, a ≤ ‖x‖ :=
  tendsto_norm_cobounded_atTop'.eventually_ge_atTop a

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