coe_lift

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.coe_lift

English

Casting the lift of x back to ENNat yields x.

Русский

Преобразование lift(x) обратно в ENNat восстанавливает x.

LaTeX

$$$$ (\\operatorname{lift}(x,h)\\; \\text{ cast}) = x. $$$$

Lean4

@[simp]
theorem coe_lift (x : ℕ∞) (h : x < ⊤) : (lift x h : ℕ∞) = x :=
  WithTop.coe_untop x (WithTop.lt_top_iff_ne_top.mp h)

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

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

Разделы

Аффилиация

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