lift_le_ofENat

Mathlib.SetTheory.Cardinal.ENat

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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