lift_eq_ofENat

Mathlib.SetTheory.Cardinal.ENat

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

English

For any x ∈ Cardinal and m ∈ ENat, lift x = m iff 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_eq_ofENat {x : Cardinal.{v}} {m : ℕ∞} : lift.{u} x = m ↔ x = m := by rw [← lift_ofENat.{u, v}, lift_inj]

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

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

Разделы

Аффилиация

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