English
If each l_i has a basis with p_i and s_i, then the supremum of all l_i has a basis with index f: ∀i, p_i (f(i)) and basic sets ⋃_i s_i (f(i)).
Русский
Если каждый l_i имеет базис (p_i, s_i), то iSup l_i имеет базис, индексации f: ∀i, p_i (f(i)) и базисные множества ⋃_i s_i (f(i)).
LaTeX
$$$\\text{HasBasis}\\left(\\bigvee_i l_i\\right)\\left(\\lambda f: \\prod_i ι' i \\mapsto \\forall i, p_i(f(i))\\right)(\\lambda f: \\prod_i ι' i \\mapsto \\bigcup_i s_i(f(i))\\right)$$$
Lean4
theorem hasBasis_iSup {ι : Sort*} {ι' : ι → 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 f : ∀ i, ι' i => ∀ i, p i (f i)) fun f : ∀ i, ι' i => ⋃ i, s i (f i) :=
hasBasis_iff.mpr fun t => by simp only [(hl _).mem_iff, Classical.skolem, forall_and, iUnion_subset_iff, mem_iSup]
