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
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