theorem String.Slice.isEmpty_eq {s : Slice} : s.isEmpty = (s.utf8ByteSize == 0)

theorem String.Slice.isEmpty_iff {s : Slice} : s.isEmpty = true ↔ s.utf8ByteSize = 0

theorem String.Slice.startPos_eq_endPos_iff {s : Slice} : s.startPos = s.endPos ↔ s.isEmpty = true

theorem String.Slice.startPos_ne_endPos_iff {s : Slice} : s.startPos ≠ s.endPos ↔ s.isEmpty = false

theorem String.Slice.startPos_ne_endPos {s : Slice} : s.isEmpty = false → s.startPos ≠ s.endPos

theorem String.Slice.isEmpty_iff_forall_eq {s : Slice} : s.isEmpty = true ↔ ∀ (p q : s.Pos), p = q

theorem String.Slice.isEmpty_eq_false_of_lt {s : Slice} {p q : s.Pos} : p < q → s.isEmpty = false

@[simp]

theorem String.Slice.isEmpty_sliceFrom {s : Slice} {p : s.Pos} : (s.sliceFrom p).isEmpty = true ↔ p = s.endPos

@[simp]

theorem String.Slice.isEmpty_sliceFrom_eq_false_iff {s : Slice} {p : s.Pos} : (s.sliceFrom p).isEmpty = false ↔ p ≠ s.endPos

@[simp]

theorem String.Slice.isEmpty_sliceTo {s : Slice} {p : s.Pos} : (s.sliceTo p).isEmpty = true ↔ p = s.startPos

@[simp]

theorem String.Slice.isEmpty_sliceTo_eq_false_iff {s : Slice} {p : s.Pos} : (s.sliceTo p).isEmpty = false ↔ p ≠ s.startPos

theorem String.isEmpty_eq_utf8ByteSize_beq_zero {s : String} : s.isEmpty = (s.utf8ByteSize == 0)

theorem String.isEmpty_iff_utf8ByteSize_eq_zero {s : String} : s.isEmpty = true ↔ s.utf8ByteSize = 0

@[simp]

theorem String.isEmpty_iff {s : String} : s.isEmpty = true ↔ s = ""

theorem String.startPos_ne_endPos_iff {s : String} : s.startPos ≠ s.endPos ↔ s ≠ ""

theorem String.startPos_ne_endPos {s : String} : s ≠ "" → s.startPos ≠ s.endPos

@[simp]

theorem String.isEmpty_toSlice {s : String} : s.toSlice.isEmpty = s.isEmpty

theorem String.isEmpty_toSlice_iff {s : String} : s.toSlice.isEmpty = true ↔ s = ""

theorem String.Slice.isEmpty_copy {s : Slice} : s.copy.isEmpty = s.isEmpty

@[simp]

theorem String.Slice.copy_eq_empty_iff {s : Slice} : s.copy = "" ↔ s.isEmpty = true

theorem String.Slice.copy_ne_empty_iff {s : Slice} : s.copy ≠ "" ↔ s.isEmpty = false

theorem String.eq_empty_iff_forall_eq {s : String} : s = "" ↔ ∀ (p q : s.Pos), p = q

theorem String.ne_empty_of_lt {s : String} {p q : s.Pos} : p < q → s ≠ ""

@[simp]

theorem String.isEmpty_sliceFrom {s : String} {p : s.Pos} : (s.sliceFrom p).isEmpty = true ↔ p = s.endPos

@[simp]

theorem String.isEmpty_sliceFrom_eq_false_iff {s : String} {p : s.Pos} : (s.sliceFrom p).isEmpty = false ↔ p ≠ s.endPos

@[simp]

theorem String.isEmpty_sliceTo {s : String} {p : s.Pos} : (s.sliceTo p).isEmpty = true ↔ p = s.startPos

@[simp]

theorem String.isEmpty_sliceTo_eq_false_iff {s : String} {p : s.Pos} : (s.sliceTo p).isEmpty = false ↔ p ≠ s.startPos

@[simp]

theorem String.isEmpty_slice {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} : (s.slice p₁ p₂ h).isEmpty = true ↔ p₁ = p₂

@[simp]

theorem String.isEmpty_slice_eq_false_iff {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} : (s.slice p₁ p₂ h).isEmpty = false ↔ p₁ ≠ p₂

@[simp]

theorem String.Slice.isEmpty_slice {s : Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} : (s.slice p₁ p₂ h).isEmpty = true ↔ p₁ = p₂

@[simp]

theorem String.Slice.isEmpty_slice_eq_false_iff {s : Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} : (s.slice p₁ p₂ h).isEmpty = false ↔ p₁ ≠ p₂

@[simp]

theorem String.length_eq_zero_iff {s : String} : s.length = 0 ↔ s = ""

@[simp]

theorem String.toByteArray_eq_empty_iff {s : String} : s.toByteArray = ByteArray.empty ↔ s = ""

theorem String.Slice.toByteArray_copy_eq_empty_iff {s : Slice} : s.copy.toByteArray = ByteArray.empty ↔ s.isEmpty = true

theorem String.Slice.toByteArray_copy_ne_empty_iff {s : Slice} : s.copy.toByteArray ≠ ByteArray.empty ↔ s.isEmpty = false