English
Applying a map F coordinatewise preserves a subset relation of loci: the locus after mapping is contained in the original locus.
Русский
Пусть применяется отображение по координатам; локус после отображения содержится в исходном локусе.
LaTeX
$$$ (f.mapRange F F0) \neLocus (g.mapRange F F0) \subseteq f.neLocus g $$$
Lean4
theorem subset_mapRange_neLocus [∀ 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) : (f.mapRange F F0).neLocus (g.mapRange F F0) ⊆ f.neLocus g := fun a ↦ by
simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg (F a)