trans_isBigOWith — Mathlib

English

If f = o_l g and IsBigOWith c l g k holds with c > 0, then f = o_l k.

Русский

Если f = o_l g и IsBigOWith c l g k выполняется при c > 0, тогда f = o_l k.

LaTeX

$$$f = o\; l\; g \land IsBigOWith\; c\; l\; g\; k \land 0 < c \Rightarrow f = o\; l\; k$$$

Lean4

theorem trans_isBigOWith (hfg : f =o[l] g) (hgk : IsBigOWith c l g k) (hc : 0 < c) : f =o[l] k :=
  by
  simp only [IsLittleO_def] at *
  intro c' c'pos
  have : 0 < c' / c := div_pos c'pos hc
  exact ((hfg this).trans hgk this.le).congr_const (div_mul_cancel₀ _ hc.ne')

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