eq_zero_iff — Mathlib

English

If f'' =Θ[l] g'' then eventually f''(x) = 0 if and only if g''(x) = 0.

Русский

Если f'' =Θ[l] g'', то с некоторого момента равно нулю значения f'' совпадает по нулю значения g''.

LaTeX

$$$ (f'' =\Theta[l] g'') \Rightarrow \forall^{\!} x \in l,\; f''(x)=0 \iff g''(x)=0. $$$

Lean4

theorem eq_zero_iff (h : f'' =Θ[l] g'') : ∀ᶠ x in l, f'' x = 0 ↔ g'' x = 0 :=
  h.1.eq_zero_imp.mp <| h.2.eq_zero_imp.mono fun _ ↦ Iff.intro

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