English
If la and lb have p-homogeneous bases sa and sb that are monotone on {i | p(i)}, then the product has basis with sa(i) × sb(i).
Русский
Если la и lb имеют монотонные базисы по p и sa, sb монотонны на {i | p(i)}, то произведение имеет базис sa(i) × sb(i).
LaTeX
$$HasBasis.prod_same_index_mono ha hb hsa hsb.$$
Lean4
/-- The smallest filter basis containing a given collection of sets. -/
def ofSets (s : Set (Set α)) : FilterBasis α
where
sets := sInter '' {t | Set.Finite t ∧ t ⊆ s}
nonempty := ⟨univ, ∅, ⟨⟨finite_empty, empty_subset s⟩, sInter_empty⟩⟩
inter_sets := by
rintro _ _ ⟨a, ⟨fina, suba⟩, rfl⟩ ⟨b, ⟨finb, subb⟩, rfl⟩
exact ⟨⋂₀ (a ∪ b), mem_image_of_mem _ ⟨fina.union finb, union_subset suba subb⟩, (sInter_union _ _).subset⟩
