lift_le_ofNat_iff

Mathlib.SetTheory.Cardinal.Order

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

English

For all a, 1 ≤ lift(a) iff 1 ≤ a.

Русский

Для всех a: 1 ≤ lift(a) эквивалентно 1 ≤ a.

LaTeX

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

Lean4

@[simp]
theorem lift_le_ofNat_iff {a : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] : lift.{v} a ≤ ofNat(n) ↔ a ≤ OfNat.ofNat n :=
  lift_le_nat_iff

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

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

Разделы

Аффилиация

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