Theorems · Theorem · general topology

Filter.mem_traverse

∀ {α β γ : 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

Defined in

Mathlib.Order.Filter.ListTraverse

Cited by

2 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound