restrictDom_apply — Mathlib

English

RestrictDom acts as filtering, restricting a finsupp to the elements in a set s, giving a linear map to the supported submodule on s.

Русский

RestrictDom реализует фильтрацию, ограничивая finsupp до элементов множества s и давая линейное отображение в поддерживаемый на s подмодуль.

LaTeX

$$$\mathrm{restrictDom}(M,R,s) : (\alpha \to_0 M) \to\mathrm{supported}(M,R,s)$$$

Lean4

@[simp]
theorem restrictDom_apply (s : Set α) (l : α →₀ M) [DecidablePred (· ∈ s)] :
    (restrictDom M R s l : α →₀ M) = Finsupp.filter (· ∈ s) l :=
  rfl

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