neLocus_sub_right — Mathlib

English

For finitely supported functions, neLocus(f1 − g, f2 − g) = neLocus(f1, f2).

Русский

Для функций с конечной опорой неравная локация удовлетворяет: neLocus(f1 − g, f2 − g) = neLocus(f1, f2).

LaTeX

$$$ neLocus (f_1 - g) (f_2 - g) = neLocus f_1 f_2 $$$

Lean4

@[simp]
theorem neLocus_sub_right : neLocus (f₁ - g) (f₂ - g) = neLocus f₁ f₂ := by
  simpa only [sub_eq_add_neg] using neLocus_add_right _ _ _

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