typo 8.1.13 ex 17 #29
Description
typo at 8.1.13 (functions) ex 17
lemma lt_trichotomy (x y : ℚ) : x < y ∨ x = y ∨ x < y :=
should be
lemma lt_trichotomy (x y : ℚ) : x < y ∨ x = y ∨ y < x :=
the last x < y should be y < x
{{ message }}
typo at 8.1.13 (functions) ex 17
lemma lt_trichotomy (x y : ℚ) : x < y ∨ x = y ∨ x < y :=
should be
lemma lt_trichotomy (x y : ℚ) : x < y ∨ x = y ∨ y < x :=
the last x < y should be y < x