toList_nonempty — Mathlib

English

Every nonempty string s satisfies s.toList = (s.head) :: (s.drop 1).toList.

Русский

Для непустой строки s выполняется s.toList = (s.head) :: (s.drop(1)).toList.

LaTeX

$$$ \forall s, s \neq \"\" \Rightarrow s.toList = (s.head) :: (s.drop(1)).toList. $$$

Lean4

theorem toList_nonempty : ∀ {s : String}, s ≠ "" → s.toList = s.head :: (s.drop 1).toList
  | ⟨s⟩, h => by
    cases s with
    | nil => simp at h
    | cons c
      cs =>
      simp only [toList, data_drop, List.drop_succ_cons, List.drop_zero, List.cons.injEq, and_true]
      rfl

Похожие утверждения