zipWith_neLocus_eq_left — Mathlib

English

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

Русский

При точной инекции по второму аргументу в F, локус zipWith равен локусу левых аргументов.

LaTeX

$$$ (zipWith F F0 f g_1).neLocus (zipWith F F0 f g_2) = g_1.neLocus g_2 $$$

Lean4

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

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