mapRange_neLocus_eq — Mathlib

English

If F is pointwise injective, then mapping f and g via mapRange preserves a difference-locus equality: (f.mapRange F F0) and (g.mapRange F F0) have the same neLocus as f and g.

Русский

Если F инъективен по каждому аргументу, отображение f и g через mapRange сохраняет равенство локусов различий: neLocus совпадает.

LaTeX

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

Lean4

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

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