Theorems · Theorem · general topology

Filter.mem_traverse_iff

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

Defined in

Mathlib.Order.Filter.ListTraverse

Cited by

1 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound