English
If f has a basis (p, s) and for each i, g(s i) has a basis (pg i, sg i), then a precise mem_iff for f.lift g holds: s ∈ f.lift g iff ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s.
Русский
Если f имеет базис (p, s), и для каждого i f(s i) имеет базис (pg i, sg i), то верно mem_iff для f.lift g: s ∈ f.lift g ⇔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s.
LaTeX
$$$s \\in f.lift g \\iff \\exists i, p i \\land \\exists x, pg i x \\land sg i x \\subseteq s$$$
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
`Filter.HasBasis` one has to use `Σ i, β i` as the index type, see `Filter.HasBasis.lift`.
This lemma states the corresponding `mem_iff` statement without using a sigma type. -/
theorem mem_lift_iff {ι} {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) {s : Set γ} : s ∈ f.lift g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s :=
by
refine (mem_biInf_of_directed ?_ ⟨univ, univ_sets _⟩).trans ?_
· intro t₁ ht₁ t₂ ht₂
exact ⟨t₁ ∩ t₂, inter_mem ht₁ ht₂, gm inter_subset_left, gm inter_subset_right⟩
· simp only [← (hg _).mem_iff]
exact hf.exists_iff fun t₁ t₂ ht H => gm ht H
