toWithTop_lt — Mathlib

English

The map toWithTop is strictly order-preserving: toWithTop x < toWithTop y iff x < y.

Русский

toWithTop строго сохраняет порядок: toWithTop x < toWithTop y тогда и только тогда x < y.

LaTeX

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

Lean4

@[simp]
theorem toWithTop_lt {x y : PartENat} [Decidable x.Dom] [Decidable y.Dom] : toWithTop x < toWithTop y ↔ x < y :=
  lt_iff_lt_of_le_iff_le toWithTop_le

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