English
If l and l' have bases with p, s and p', s', then the supremum l ⊔ l' has a basis given by p i.1 ∧ p' i.2 with basic sets s i.1 ∪ s' i.2.
Русский
Если у l и l' есть базы (p, s) и (p', s'), то их объединение l ⊔ l' имеет базис, индексируемый попарно, с базисными множествами s_i ∪ s'_j.
LaTeX
$$$\\text{HasBasis}\\left(l \\!\\sups\\! l'\\right)\\left(\\lambda i : PProd ι ι' \\mapsto p(i.1) \\land p'(i.2)\\right)(\\lambda i : PProd ι ι' \\mapsto s(i.1) \\cup s'(i.2)\\right)$$$
Lean4
theorem sup' (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
(l ⊔ l').HasBasis (fun i : PProd ι ι' => p i.1 ∧ p' i.2) fun i => s i.1 ∪ s' i.2 :=
⟨by
intro t
simp_rw [mem_sup, hl.mem_iff, hl'.mem_iff, PProd.exists, union_subset_iff, ← exists_and_right, ← exists_and_left]
simp only [and_assoc, and_left_comm]⟩
