isTheta_congr_right — Mathlib

English

If two functions f' and g' are Θ-equivalent along a filter l, then for any third function k, k is Θ-along l with f' if and only if k is Θ-along l with g'. In other words, right-Θ-congruence holds: f' =Θ_l g' implies k =Θ_l f' ⇔ k =Θ_l g'.

Русский

Если две функции f' и g' эквивалентны по Θ-отношению вдоль фильтра l, то для любой третьей функции k равенство k =Θ_l f' эквивалентно k =Θ_l g'. Иными словами, правая конгруэнтность относительно Θ сохраняется: f' =Θ_l g' ⇒ k =Θ_l f' ⇔ k =Θ_l g'.

LaTeX

$$$ f' =\Theta_{l} g' \Rightarrow (k =\Theta_{l} f' \Leftrightarrow k =\Theta_{l} g') $$$

Lean4

theorem isTheta_congr_right (h : f' =Θ[l] g') : k =Θ[l] f' ↔ k =Θ[l] g' :=
  h.isBigO_congr_right.and h.isBigO_congr_left

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