Documentation

Mathlib.Order.Filter.ListTraverse

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 (x1 x2 : Filter α) => x1 x2) as bssequence 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 ustraverse 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