basisRestrictSupport — Mathlib

English

restrictSupport R s has a canonical basis indexed by s.

Русский

restrictSupport R s имеет каноническую базу, индексируемую по s.

LaTeX

$$$\\text{basisRestrictSupport}(s) : \\text{Basis } s\\, R\\, (\\mathrm{restrictSupport}\\ R\\ s)$$$

Lean4

/-- `restrictSupport R s` has a canonical `R`-basis indexed by `s`. -/
def basisRestrictSupport (s : Set (σ →₀ ℕ)) : Basis s R (restrictSupport R s) where
  repr := Finsupp.supportedEquivFinsupp s

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