subset_mapRange_neLocus — Mathlib

English

If F: N → M with F(0)=0, then (f.mapRange F F0).neLocus (g.mapRange F F0) ⊆ f.neLocus g.

Русский

При F: N → M, F(0)=0, имеем (f.mapRange F F0).neLocus (g.mapRange F F0) ⊆ f.neLocus g.

LaTeX

$$$$ (f.mapRange F F0).neLocus (g.mapRange F F0) \subseteq f.neLocus g. $$$$

Lean4

theorem subset_mapRange_neLocus [DecidableEq N] [Zero N] [DecidableEq M] [Zero M] (f g : α →₀ N) {F : N → M}
    (F0 : F 0 = 0) : (f.mapRange F F0).neLocus (g.mapRange F F0) ⊆ f.neLocus g := fun x => by
  simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg F

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