zipWith_neLocus_eq_right — Mathlib

English

If F is injective in the first argument, then (zipWith F F0 f1 g).neLocus (zipWith F F0 f2 g) = f1.neLocus f2 g.

Русский

Если F инъективен по первому аргументу, то neLocus сохраняется в правой части.

LaTeX

$$$$ (zipWith F F0 f_1 g).neLocus (zipWith F F0 f_2 g) = f_1.neLocus f_2. $$$$

Lean4

theorem zipWith_neLocus_eq_right [DecidableEq M] [Zero M] [DecidableEq P] [Zero P] [Zero N] {F : M → N → P}
    (F0 : F 0 0 = 0) (f₁ f₂ : α →₀ M) (g : α →₀ N) (hF : ∀ g, Function.Injective fun f => F f g) :
    (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂ :=
  by
  ext
  simpa only [mem_neLocus] using (hF _).ne_iff

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