mem_takeWhile_imp — Mathlib

English

Let x be an element; if x belongs to takeWhile p l, then p x is true.

Русский

Пусть x — элемент; если x принадлежит takeWhile p l, то p x истинно.

LaTeX

$$$\\text{If } x \\in \\mathrm{takeWhile}(p, l) \\text{ then } p(x) = \\text{true}$$$

Lean4

theorem mem_takeWhile_imp {x : α} (hx : x ∈ takeWhile p l) : p x := by
  induction l with simp [takeWhile] at hx
  | cons hd tl IH =>
    cases hp : p hd
    · simp [hp] at hx
    · rw [hp, mem_cons] at hx
      rcases hx with (rfl | hx)
      · exact hp
      · exact IH hx

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