exists_eq_mul — Mathlib

English

If IsBigOWith(c, l, u, v) holds and c ≥ 0, there exists φ with ‖φ‖ ≤ c and u =ᶠ[l] φ · v.

Русский

Если IsBigOWith(c, l, u, v) выполняется и c ≥ 0, существует φ с ‖φ‖ ≤ c и u =ᶠ[l] φ · v.

LaTeX

$$$ IsBigOWith\\ c\\ l\\ u\\ v \\Rightarrow \\Exists \\phi : α \\to 𝕜, (\\forallᶠ x in l, \\|\\phi x\\| ≤ c) ∧ u =ᶠ[l] \\phi \\cdot v $$$

Lean4

theorem exists_eq_mul (h : IsBigOWith c l u v) (hc : 0 ≤ c) : ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v :=
  (isBigOWith_iff_exists_eq_mul hc).mp h

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