le_eqLocus — Mathlib

English

For two maps f and g between modules and a submodule S, f and g agree on S if and only if S is contained in the locus where f equals g.

Русский

Для двух отображений f и g между модулями и подмодуля S верно: f и g согласованы на S тогда и только тогда, когда S входит в локус, где f = g.

LaTeX

$$$S \\leeq eqLocus(f,g) \\iff (\\forall x \\in S, f(x) = g(x))$$$

Lean4

theorem le_eqLocus {f g : F} {S : Submodule R M} : S ≤ eqLocus f g ↔ Set.EqOn f g S :=
  Iff.rfl

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