small

Mathlib.Data.DFinsupp.Small

URI: https://scilib.ai/kg/mathlib#Finsupp.small

← MathLib Explorer

English

If σ is small and R is small (with Zero), then Finsupp σ R is small.

Русский

Если σ и R малы, то Finsupp σ R также мал.

LaTeX

$$[Small σ] [Small R] ⇒ Small(σ →₀ R)$$

Lean4

instance small {σ : Type*} {R : Type*} [Zero R] [Small.{u} R] [Small.{u} σ] : Small.{u} (σ →₀ R) := by
  classical exact small_map finsuppEquivDFinsupp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru