zero_lt_lift_iff

Mathlib.SetTheory.Cardinal.Order

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

English

The lifted cardinal is positive if and only if the original cardinal is positive.

Русский

Поднятый кардинал положителен тогда и только тогда, когда исходный кардинал положителен.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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