congr — Mathlib

English

Let f1 = O_l(g1). If f1 equals f2 pointwise and g1 equals g2 pointwise, then f2 = O_l(g2).

Русский

Пусть f1 = O_l(g1). Если f1(x) = f2(x) для всех x и g1(x) = g2(x) для всех x, тогда f2 = O_l(g2).

LaTeX

$$$ (f_1 = O[l]\, g_1) \land (\forall x,\; f_1(x)=f_2(x)) \land (\forall x,\; g_1(x)=g_2(x)) \Rightarrow f_2 = O[l]\, g_2 $$$

Lean4

theorem congr (h : f₁ =O[l] g₁) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) : f₂ =O[l] g₂ :=
  h.congr' (univ_mem' hf) (univ_mem' hg)

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