Lift filters along filter and set functions #
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.
If (p : ι → Prop, s : ι → set α)
is a basis of a filter f
, g
is a monotone function
set α → filter γ
, and for each i
, (pg : β i → Prop, sg : β i → set α)
is a basis
of the filter g (s i)
, then (λ (i : ι) (x : β i), p i ∧ pg i x, λ (i : ι) (x : β i), sg i x)
is a basis of the filter f.lift g
.
This basis is parametrized by i : ι
and x : β i
, so in order to formulate this fact using
has_basis
one has to use Σ i, β i
as the index type, see filter.has_basis.lift
.
This lemma states the corresponding mem_iff
statement without using a sigma type.
If (p : ι → Prop, s : ι → set α)
is a basis of a filter f
, g
is a monotone function
set α → filter γ
, and for each i
, (pg : β i → Prop, sg : β i → set α)
is a basis
of the filter g (s i)
, then (λ (i : ι) (x : β i), p i ∧ pg i x, λ (i : ι) (x : β i), sg i x)
is a basis of the filter f.lift g
.
This basis is parametrized by i : ι
and x : β i
, so in order to formulate this fact using
has_basis
one has to use Σ i, β i
as the index type. See also filter.has_basis.mem_lift_iff
for the corresponding mem_iff
statement formulated without using a sigma type.