English
TakeWhile with a fixed predicate p is idempotent on lists: for every list l and predicate p, takeWhile p (takeWhile p l) = takeWhile p l.
Русский
TakeWhile по фиксированному предикату p является идемпотентным на списках: для любого списка l и предиката p выполняется takeWhile p (takeWhile p l) = takeWhile p l.
LaTeX
$$$$\\forall l:\\, \\text{List}~\\alpha,\\; \\forall p:\\, \\alpha \\rightarrow \\text{Bool},\\; \\operatorname{takeWhile}(p, \\operatorname{takeWhile}(p, l)) = \\operatorname{takeWhile}(p, l).$$$$
Lean4
theorem takeWhile_idem : takeWhile p (takeWhile p l) = takeWhile p l := by
simp_rw [takeWhile_takeWhile, and_self_iff, Bool.decide_coe]
