Theorems · Theorem · general topology

Filter.seq_assoc

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Filter α) (g : Filter (α → β)) (h : Filter (β → γ)),
  h.seq (g.seq x) = ((Filter.map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x

Defined in

Mathlib.Order.Filter.Map

Cited by

0 results in Mathlib

Foundations

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