subset_mapRange_neLocus — Mathlib

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)

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