neLocus_eq_support_sub — Mathlib

English

The set of coordinates where f and g differ is exactly the support of their difference f − g: f.neLocus g = (f − g).support.

Русский

Множество координат, на которых f и g различаются, ровно опорa разности f − g: f.neLocus g = (f − g).support.

LaTeX

$$$ f.neLocus g = (f - g).\mathrm{support} $$$

Lean4

theorem neLocus_eq_support_sub : f.neLocus g = (f - g).support := by
  rw [← neLocus_add_right _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]

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