Further results about UTF-8 decoding

@[simp]

theorem String.utf8EncodeChar_lt_utf8EncodeChar_iff {c d : Char} : utf8EncodeChar c < utf8EncodeChar d ↔ c < d

@[simp]

theorem String.compare_utf8EncodeChar_utf8EncodeChar {c d : Char} : compare (utf8EncodeChar c) (utf8EncodeChar d) = compare c d

@[simp]

theorem String.utf8EncodeChar_le_utf8EncodeChar_iff {c d : Char} : utf8EncodeChar c ≤ utf8EncodeChar d ↔ c ≤ d

theorem String.compare_toList_toList_eq_compare_toByteArray_toByteArray {s t : String} : compare s.toList t.toList = compare s.toByteArray t.toByteArray

theorem String.toList_lt_toList_iff_toByteArray_lt_toByteArray {s t : String} : s.toList < t.toList ↔ s.toByteArray < t.toByteArray

theorem String.toList_le_toList_iff_toByteArray_le_toByteArray {s t : String} : s.toList ≤ t.toList ↔ s.toByteArray ≤ t.toByteArray