English
If l has a basis with p and s, and l′ with p′ and s′, then their supremum has a basis indexed by pairs, with basic unions of the corresponding base sets.
Русский
Если филтр l имеет базис с p, s, а l′ — с p′, s′, то их супремум имеет базис, индексируемый парами, и базисные множества — объединения соответствующих базисных множеств.
LaTeX
$$$\\text{HasBasis}(l)\\rightarrow \\text{HasBasis}(l')\\rightarrow \\text{HasBasis}(l \\vee l')(i) = s(i.1) \\cup s'(i.2)\\text{ для } p(i.1) \\land p'(i.2)$$$
Lean4
theorem sup {ι ι' : Type*} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : l.HasBasis p s)
(hl' : l'.HasBasis p' s') : (l ⊔ l').HasBasis (fun i : ι × ι' => p i.1 ∧ p' i.2) fun i => s i.1 ∪ s' i.2 :=
(hl.sup' hl').comp_equiv Equiv.pprodEquivProd.symm
