toWithTop_le — Mathlib

English

The map toWithTop preserves order: for all x,y, toWithTop x ≤ toWithTop y iff x ≤ y.

Русский

Отображение toWithTop сохраняет порядок: для всех x,y выполняется toWithTop x ≤ toWithTop y тогда и только тогда x ≤ y.

LaTeX

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

Lean4

@[simp]
theorem toWithTop_le {x y : PartENat} [hx : Decidable x.Dom] [hy : Decidable y.Dom] :
    toWithTop x ≤ toWithTop y ↔ x ≤ y :=
  by
  induction y using PartENat.casesOn generalizing hy
  · simp
  induction x using PartENat.casesOn generalizing hx
  · simp
  · simp

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