support_extendDomain_subset — Mathlib

English

If f is a finitely supported function on the subtype P, then the support of its extension to the ambient type lies inside the set {x | P x}.

Русский

Пусть f: Subtype P →₀ M. Тогда поддержка f.extendDomain лежит внутри множества {x | P x}.

LaTeX

$$$\\uparrow( f.\\mathrm{extendDomain}).\\mathrm{support} \\subseteq \\{ x \\mid P x \\}$$$

Lean4

theorem support_extendDomain_subset (f : Subtype P →₀ M) : ↑(f.extendDomain).support ⊆ {x | P x} :=
  by
  intro x
  rw [extendDomain_support, mem_coe, mem_map, Embedding.coe_subtype]
  rintro ⟨x, -, rfl⟩
  exact x.prop

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