small_zero

Mathlib.Logic.Small.Defs

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

English

For every α, Small^{w} α.

Русский

Для всякого α верно Small^{w} α.

LaTeX

$$$\forall \alpha, Small^{w}(\alpha).$$$

Lean4

instance small_zero (α : Type) : Small.{w} α :=
  small_max α

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

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

Разделы

Аффилиация

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