subtypeDomainLinearMap — Mathlib

English

The subtype-domain restriction functor is linear, i.e., a linear map from DFinsupp to functions on a subtype.

Русский

Ограничение по подтипу области образует линейное отображение от DFinsupp к функциям на подмножестве.

LaTeX

$$$$ \\mathrm{subtypeDomainLinearMap}: (\\\\Pi_i β_i) \\to_{\\\\ell} (\\\\Pi_{i:\\\\mathrm{Subtype}(p)} β_i) $$$$

Lean4

/-- `DFinsupp.subtypeDomain` as a `LinearMap`. -/
@[simps]
def subtypeDomainLinearMap [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] (p : ι → Prop)
    [DecidablePred p] : (Π₀ i, β i) →ₗ[γ] Π₀ i : Subtype p, β i
    where
  toFun := subtypeDomain p
  map_add' := subtypeDomain_add
  map_smul' := subtypeDomain_smul

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