smallList

Mathlib.Logic.Small.List

URI: https://scilib.ai/kg/mathlib#smallList

← MathLib Explorer

English

If α is Small, then List α is Small.

Русский

Если α мала, то List α мала.

LaTeX

$$$\forall \alpha, Small(\alpha) \Rightarrow Small(\mathrm{List}(\alpha)).$$$

Lean4

instance smallList {α : Type v} [Small.{u} α] : Small.{u} (List α) :=
  by
  let e : (Σ n, List.Vector α n) ≃ List α := Equiv.sigmaFiberEquiv List.length
  exact small_of_surjective e.surjective

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

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

Разделы

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

Аффилиация

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