neLocus_sub_left — Mathlib

English

For finitely supported functions, neLocus(f − g1, f − g2) = g1.neLocus(g2).

Русский

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

LaTeX

$$$ neLocus (f - g_1) (f - g_2) = neLocus g_1 g_2 $$$

Lean4

@[simp]
theorem neLocus_sub_left : neLocus (f - g₁) (f - g₂) = neLocus g₁ g₂ := by
  simp only [sub_eq_add_neg, neLocus_add_left, neLocus_neg_neg]

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