small_succ

Mathlib.Logic.Small.Defs

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

English

For every α, Small^{v+1} α.

Русский

Для каждого α верно Small^{v+1} α.

LaTeX

$$$\forall \alpha, Small^{v+1}(\alpha).$$$

Lean4

instance (priority := 100) small_succ (α : Type v) : Small.{v + 1} α :=
  small_lift.{v, v + 1} α

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

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

Разделы

Аффилиация

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