trans — Mathlib

English

If f =OWith c l f g and g =OWith c' l g k, then f =OWith (c c') l f k (with 0 ≤ c).

Русский

Если f =OWith c l f g и g =OWith c' l g k, то f =OWith (c c') l f k (при 0 ≤ c).

LaTeX

$$$f = OWith\; c\; l\; f\; g \quad\land\quad g = OWith\; c'\; l\; g\; k \;\Rightarrow\; f = OWith\; (c c')\; l\; f\; k,\quad 0 \le c$$$

Lean4

theorem trans (hfg : IsBigOWith c l f g) (hgk : IsBigOWith c' l g k) (hc : 0 ≤ c) : IsBigOWith (c * c') l f k :=
  by
  simp only [IsBigOWith_def] at *
  filter_upwards [hfg, hgk] with x hx hx'
  calc
    ‖f x‖ ≤ c * ‖g x‖ := hx
    _ ≤ c * (c' * ‖k x‖) := by gcongr
    _ = c * c' * ‖k x‖ := (mul_assoc _ _ _).symm

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