ofENat_eq_lift

Mathlib.SetTheory.Cardinal.ENat

URI: https://scilib.ai/kg/mathlib#Cardinal.ofENat_eq_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_eq_lift {x : Cardinal.{v}} {m : ℕ∞} : m = lift.{u} x ↔ m = x := by rw [← lift_ofENat.{u, v}, lift_inj]

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

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

Разделы

Аффилиация

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