ofENat_le_lift

Mathlib.SetTheory.Cardinal.ENat

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

English

For any x ∈ Cardinal and m ∈ ENat, m ≤ lift x ↔ m ≤ x.

Русский

Для любого x ∈ Cardinal и m ∈ ENat, m ≤ lift x ↔ m ≤ x.

LaTeX

$$∀ {x : Cardinal} {m : \mathbb{N}_\infty}, m ≤ lift x ↔ m ≤ x$$

Lean4

@[simp]
theorem ofENat_le_lift {x : Cardinal.{v}} {m : ℕ∞} : m ≤ lift.{u} x ↔ m ≤ x := by rw [← lift_ofENat.{u, v}, lift_le]

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

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

Разделы

Аффилиация

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