English
Let fs: List β and us: List γ with Forall₂ (s c ∈ f b) fs.us; then traverse s us ∈ traverse f fs.
Русский
Пусть fs: список β и us: список γ удовлетворяют Forall₂ (s c ∈ f b) fs us; тогда traverse s us ∈ traverse f fs.
LaTeX
$$$\\text{Forall₂} (\\mathsf{mem}\\, (f b))\, fs\, us \\\\Rightarrow \\text{traverse}\\, s\\, us \\in \\text{traverse}\\, f\\, fs$$$
Lean4
theorem mem_traverse :
∀ (fs : List β) (us : List γ), Forall₂ (fun b c => s c ∈ f b) fs us → traverse s us ∈ traverse f fs
| [], [], Forall₂.nil => mem_pure.2 <| mem_singleton _
| _ :: fs, _ :: us, Forall₂.cons h hs =>
seq_mem_seq (image_mem_map h)
(mem_traverse fs us hs)
-- TODO: add a `Filter.HasBasis` statement
