Theorems · Theorem · general topology

Filter.lift_iInf_of_directed

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Nonempty ι] {f : ι → Filter α} {g : Set α → Filter β},
  Directed (fun x1 x2 => x1 ≥ x2) f → Monotone g → (iInf f).lift g = ⨅ i, (f i).lift g

Defined in

Mathlib.Order.Filter.Lift

Cited by

0 results in Mathlib

Foundations

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

Assumes

Nonempty