coe_lt_coe — Mathlib

English

If α has a linear order, then the embedding preserves the strict order: (a : WithTop α) < b iff a < b.

Русский

Если у α есть строгий порядок, то вложение сохраняет строгий порядок: (a : WithTop α) < b эквивалентно a < b.

LaTeX

$$$\forall \{a,b\},\ (a : \mathrm{WithTop}(\alpha)) < b \iff a < b$$$

Lean4

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

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