one_lt_lift_iff

Mathlib.SetTheory.Cardinal.Order

URI: https://scilib.ai/kg/mathlib#Cardinal.one_lt_lift_iff

English

For all cardinals a, 1 < lift(a) iff 1 < a.

Русский

Для любого кардинала a верно, что 1 < lift(a) тогда и только тогда, когда 1 < a.

LaTeX

$$$1 < \operatorname{lift}(a) \iff 1 < a$$$

Lean4

@[simp]
theorem one_lt_lift_iff {a : Cardinal.{u}} : (1 : Cardinal) < lift.{v} a ↔ 1 < a := by
  simpa using nat_lt_lift_iff (n := 1)

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

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

Разделы

Аффилиация

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