splitOnP_eq_single — Mathlib

English

If p holds for no element of xs, then xs.splitOnP p equals [xs].

Русский

Если для всех x из xs p x ложно, то xs.splitOnP p = [xs].

LaTeX

$$$\\forall {\\alpha} (p: \\alpha \\to \\mathrm{Bool}) (xs: \\mathrm{List}(\\alpha))\\; (\\forall x \\in xs, \\neg p(x)) \\Rightarrow xs.splitOnP p = [xs]$$$

Lean4

/-- If no element satisfies `p` in the list `xs`, then `xs.splitOnP p = [xs]` -/
theorem splitOnP_eq_single (h : ∀ x ∈ xs, ¬p x) : xs.splitOnP p = [xs] := by
  induction xs with
  | nil => simp only [splitOnP_nil]
  | cons hd tl ih =>
    simp only [splitOnP_cons, h hd mem_cons_self, if_false, Bool.false_eq_true, modifyHead_cons,
      ih <| forall_mem_of_forall_mem_cons h]

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