Theorems · Definition · general topology

Filter.lift

{α : Type u_1} → {β : Type u_2} → Filter α → (Set α → Filter β) → Filter β

A variant on bind using a function g taking a set instead of a member of α. This is essentially a push-forward along a function mapping each set to a filter.

Defined in

Mathlib.Order.Filter.Defs

Cited by

45 results in Mathlib

Foundations

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