mapRange_neLocus_eq — Mathlib

English

If F is injective, then (f.mapRange F F0).neLocus (g.mapRange F F0) = f.neLocus g.

Русский

Если F инъективен, то (f.mapRange F F0).neLocus (g.mapRange F F0) = f.neLocus g.

LaTeX

$$$$ (f.mapRange F F0).neLocus (g.mapRange F F0) = f.neLocus g. $$$$

Lean4

theorem mapRange_neLocus_eq [DecidableEq N] [DecidableEq M] [Zero M] [Zero N] (f g : α →₀ N) {F : N → M} (F0 : F 0 = 0)
    (hF : Function.Injective F) : (f.mapRange F F0).neLocus (g.mapRange F F0) = f.neLocus g :=
  by
  ext
  simpa only [mem_neLocus] using hF.ne_iff

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