English
If p holds for all elements of s, then p holds for any x ∈ take n s.
Русский
Если p выполняется для всех элементов s, то p выполняется и для любого x, принадлежащего take n s.
LaTeX
$$$\forall s\,\forall p,\ (\forall x\in s,\ p x) \rightarrow \forall n,\ \forall x,\ x\in\ take\ n\ s\rightarrow p x$$$
Lean4
theorem take_all {s : Seq α} {p : α → Prop} (h_all : ∀ x ∈ s, p x) {n : ℕ} {x : α} (hx : x ∈ s.take n) : p x := by
induction n generalizing s with
| zero => simp [take] at hx
| succ m ih =>
cases s with
| nil => simp at hx
| cons hd tl =>
simp only [take_succ_cons, List.mem_cons, mem_cons_iff, forall_eq_or_imp] at hx h_all
rcases hx with (rfl | hx)
exacts [h_all.left, ih h_all.right hx]
