English
If f has a basis and for each i, g(s i) has a basis, and g is monotone, then f.lift g has a basis given by combining the bases.
Русский
Если у f есть базис, для каждого i у g(s i) есть базис и g монотонен, то f.lift g имеет базис, полученный от сочетания базисов.
LaTeX
$$$(f.HasBasis p s) \\to \\big(\\forall i, (g(s i)).HasBasis (pg i) (sg i)\\big) \\to (\\text{Monotone } g) \\to (f.lift g).HasBasis (\\lambda i. (p i.1) \\land (pg i.1 i.2)) (\\lambda i. (sg i.1 i.2))$$$
Lean4
/-- 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
`(fun (i : ι) (x : β i) ↦ p i ∧ pg i x, fun (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.HasBasis.mem_lift_iff`
for the corresponding `mem_iff` statement formulated without using a sigma type. -/
theorem lift {ι} {p : ι → Prop} {s : ι → Set α} {f : Filter α} (hf : f.HasBasis p s) {β : ι → Type*}
{pg : ∀ i, β i → Prop} {sg : ∀ i, β i → Set γ} {g : Set α → Filter γ} (hg : ∀ i, (g (s i)).HasBasis (pg i) (sg i))
(gm : Monotone g) : (f.lift g).HasBasis (fun i : Σ i, β i => p i.1 ∧ pg i.1 i.2) fun i : Σ i, β i => sg i.1 i.2 :=
by
refine ⟨fun t => (hf.mem_lift_iff hg gm).trans ?_⟩
simp [Sigma.exists, and_assoc, exists_and_left]
