congr — Mathlib

English

If h : f1 = o[l] g1 and hf, hg express pointwise equalities f1 ≡ f2 and g1 ≡ g2, then f2 = o[l] g2.

Русский

Если h : f1 = o_l(g1) и hf, hg описывают побитовые равенства f1 ≡ f2 и g1 ≡ g2, тогда 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)

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