coe_lt_coe — Mathlib

English

If a,b ∈ α, then the lt relation between the coerced elements (a : WithZero α) and b coincides with the original order a < b in α.

Русский

Пусть a, b ∈ α. Отношение меньшему между приведёнными через вставку элементами (a : WithZero α) и b совпадает с нативным порядком a < b в α.

LaTeX

$$$ (a : \mathrm{WithZero} \alpha) < b \iff a < b $$$

Lean4

@[simp, norm_cast]
theorem coe_lt_coe : (a : WithZero α) < b ↔ a < b := by simp [lt_def]

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