English
The real numbers form a partial order with the usual ≤ and <, satisfying antisymmetry and the standard relation between equality and ≤, <.
Русский
Действительные образуют частичный порядок с обычными отношениями ≤ и <, удовлетворяющий антисимметрии и стандартной связи между равенством и ≤, <.
LaTeX
$$$\mathbb{R}$ with the usual $\le, <)$ is a partial order: reflexive, transitive, antisymmetric; and $a < b$ iff $a \le b$ and $a \neq b$.$$
Lean4
instance partialOrder : PartialOrder ℝ where
le := (· ≤ ·)
lt := (· < ·)
lt_iff_le_not_ge a
b := by
induction a using Real.ind_mk
induction b using Real.ind_mk
simpa using lt_iff_le_not_ge
le_refl
a := by
induction a using Real.ind_mk
rw [mk_le]
le_trans a b
c := by
induction a using Real.ind_mk
induction b using Real.ind_mk
induction c using Real.ind_mk
simpa using le_trans
le_antisymm a
b := by
induction a using Real.ind_mk
induction b using Real.ind_mk
simpa [mk_eq] using CauSeq.le_antisymm
