takeWhile_takeWhile — Mathlib

English

takeWhile p (takeWhile q l) = takeWhile (λ a. p a ∧ q a) l.

Русский

takeWhile p (takeWhile q l) = takeWhile (λ a, p a ∧ q a) l.

LaTeX

$$$\\mathrm{takeWhile}\\, p\\, (\\mathrm{takeWhile}\\, q\\, l) = \\mathrm{takeWhile}\\, (\\lambda a. p(a) \\land q(a))\\, l$$$

Lean4

theorem takeWhile_takeWhile (p q : α → Bool) (l : List α) :
    takeWhile p (takeWhile q l) = takeWhile (fun a => p a ∧ q a) l := by
  induction l with
  | nil => simp
  | cons hd tl IH => by_cases hp : p hd <;> by_cases hq : q hd <;> simp [takeWhile, hp, hq, IH]

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