lift_lt_univ'

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.lift_lt_univ'

← MathLib Explorer

English

For any c, lift^{max(u+1,v),u} c < univ^{u,v}.

Русский

Для любого c, lift^{max(u+1,v),u} c < univ^{u,v}.

LaTeX

$$$\\mathrm{lift}^{\\max(u+1,v),u}(c) < \\mathrm{univ}^{u,v}$$$

Lean4

theorem lift_lt_univ' (c : Cardinal) : lift.{max (u + 1) v, u} c < univ.{u, v} :=
  by
  have := lift_lt.{_, max (u + 1) v}.2 (lift_lt_univ c)
  rw [lift_lift, lift_univ, univ_umax.{u, v}] at this
  exact this

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

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

Разделы

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

Аффилиация

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