zipWith_neLocus_eq_right — Mathlib

English

If F is pointwise injective in its first argument, then the neLocus of zipWith F F0 over f₁ and f₂ equals the neLocus of f₁ and f₂.

Русский

Если F инъективна по первому аргументу, то локус zipWith по f₁ и f₂ совпадает с локусом f₁ и f₂.

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 [∀ a, DecidableEq (M a)] [∀ a, DecidableEq (P a)] {F : ∀ a, M a → N a → P a}
    (F0 : ∀ a, F a 0 0 = 0) (f₁ f₂ : Π₀ a, M a) (g : Π₀ a, N a) (hF : ∀ a g, Function.Injective fun f ↦ F a f g) :
    (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂ :=
  by
  ext a
  simpa only [mem_neLocus] using (hF a _).ne_iff

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