withTopEquiv_lt — Mathlib

English

For all x, y in PartENat, the strict order is preserved by withTopEquiv: withTopEquiv x < withTopEquiv y iff x < y.

Русский

Для любых x, y ∈ PartENat строгий порядок сохраняется отображением withTopEquiv: x < y тогда и только тогда, когда withTopEquiv x < withTopEquiv y.

LaTeX

$$$ withTopEquiv x < withTopEquiv y \iff x < y $$$

Lean4

theorem withTopEquiv_lt {x y : PartENat} : withTopEquiv x < withTopEquiv y ↔ x < y := by simp

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