Theorems · Theorem · general topology

Filter.lift_assoc

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Filter β} {h : Set β → Filter γ},
  Monotone g → (f.lift g).lift h = f.lift fun s => (g s).lift h

Defined in

Mathlib.Order.Filter.Lift

Cited by

3 results in Mathlib

Foundations

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