eventually_nnnorm — Mathlib

English

For an increasing approximate unit, eventually the nnorm is bounded by 1.

Русский

Для возрастающей аппроксимированной единицы в пределе nnorm ограничен единицей.

LaTeX

$$$$ \forall \text{l } \text{l.IsIncreasingApproximateUnit} \Rightarrow \forall x, \|x\|_+ \le 1 \text{ eventually } $$$$

Lean4

theorem eventually_nnnorm {l : Filter A} (hl : l.IsIncreasingApproximateUnit) : ∀ᶠ x in l, ‖x‖₊ ≤ 1 :=
  hl.eventually_norm

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