English
General construction of basis for the infimum of a family of filters: index is pairs (If, f) with If finite and f(i) in the basis of l_i.
Русский
Обобщённая конструкция базиса для пересечения семейства фильтров: индекс — пары (If, f) с If конечен и f(i) внутри базиса l_i.
LaTeX
$$HasBasis iInf describes a basis for ⨅ i, l i with a constructed index and basic sets.$$
Lean4
protected theorem iInf {ι : Type*} {ι' : ι → Type*} {l : ι → Filter α} {p : ∀ i, ι' i → Prop} {s : ∀ i, ι' i → Set α}
(hl : ∀ i, (l i).HasBasis (p i) (s i)) :
(⨅ i, l i).HasBasis (fun If : Σ I : Set ι, ∀ i : I, ι' i => If.1.Finite ∧ ∀ i : If.1, p i (If.2 i)) fun If =>
⋂ i : If.1, s i (If.2 i) :=
by
refine ⟨fun t => ⟨fun ht => ?_, ?_⟩⟩
· rcases (HasBasis.iInf' hl).mem_iff.mp ht with ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩
exact ⟨⟨I, fun i => f i⟩, ⟨hI, Subtype.forall.mpr hf⟩, trans (iInter_subtype _ _) hsub⟩
· rintro ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩
refine mem_of_superset ?_ hsub
cases hI.nonempty_fintype
exact iInter_mem.2 fun i => mem_iInf_of_mem ↑i <| (hl i).mem_of_mem <| hf _
