English
Similarly, for snoc x_init x_last forming a last element appended to an init sequence, membership in piFinset (snoc s_init s_last) is equivalent to x_last ∈ s_last and x_init ∈ piFinset s_init.
Русский
Аналогично для snoc x_init x_last: членство в piFinset (snoc s_init s_last) эквивалентно x_last ∈ s_last и x_init ∈ piFinset s_init.
LaTeX
$$$ snoc\\,x\\_init\\,x\\_last \\in \\ piFinset (snoc\\,s\\_init\\,s\\_last) \\iff x\\_last \\in s\\_last \\wedge x\\_init \\in \\ piFinset s\\_init $$$
Lean4
theorem snoc_mem_piFinset_snoc {x_last : α (last n)} {x_init : (i : Fin n) → α i.castSucc}
{s_last : Finset (α (last n))} {s_init : (i : Fin n) → Finset (α i.castSucc)} :
snoc x_init x_last ∈ piFinset (snoc s_init s_last) ↔ x_last ∈ s_last ∧ x_init ∈ piFinset s_init := by
simp_rw [mem_piFinset_iff_last_init, init_snoc, snoc_last]
