ofENat_toWithTop

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.ofENat_toWithTop

← MathLib Explorer

English

The strict order is preserved: x < y iff toWithTop x < toWithTop y.

Русский

Строгое неравенство сохраняется: x < y эквивалентно toWithTop x < toWithTop y.

LaTeX

$$$\\\\operatorname{toWithTop} x < \\\\operatorname{toWithTop} y \\\\iff x < y$$$

Lean4

@[simp, norm_cast]
theorem ofENat_toWithTop (x : PartENat) {_ : Decidable (x : PartENat).Dom} : toWithTop x = x := by
  induction x using PartENat.casesOn <;> simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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