restrictDom — Mathlib

English

The support over a family of sets equals the supremum of the supports over each member.

Русский

Опора над семейством множеств равна наибольшему объему опор по каждому элементу семейства.

LaTeX

$$$\mathrm{supported}(M,R,\bigcup_{i} s_i) = \bigvee_i \mathrm{supported}(M,R,s_i)$$$

Lean4

/-- Interpret `Finsupp.filter s` as a linear map from `α →₀ M` to `supported M R s`. -/
def restrictDom (s : Set α) [DecidablePred (· ∈ s)] : (α →₀ M) →ₗ[R] supported M R s :=
  LinearMap.codRestrict _
    { toFun := filter (· ∈ s)
      map_add' := fun _ _ => filter_add
      map_smul' := fun _ _ => filter_smul } fun l => (mem_supported' _ _).2 fun _ => filter_apply_neg (· ∈ s) l

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