Properties of Traversable.traverse on Lists and Filters

In this file we prove basic properties (monotonicity, membership) for Traversable.traverse f l, where f : β → Filter α and l : List β.

theorem Filter.sequence_mono {α : Type u} (as : List (Filter α)) (bs : List (Filter α)) : List.Forall₂ (fun (x x_1 : Filter α) => x ≤ x_1) as bs → sequence as ≤ sequence bs

theorem Filter.mem_traverse {α : Type u} {β : Type u} {γ : Type u} {f : β → Filter α} {s : γ → Set α} (fs : List β) (us : List γ) : List.Forall₂ (fun (b : β) (c : γ) => s c ∈ f b) fs us → traverse s us ∈ traverse f fs

theorem Filter.mem_traverse_iff {α : Type u} {β : Type u} {f : β → Filter α} (fs : List β) (t : Set (List α)) : t ∈ traverse f fs ↔ ∃ (us : List (Set α)), List.Forall₂ (fun (b : β) (s : Set α) => s ∈ f b) fs us ∧ sequence us ⊆ t