English
If la and lb have bases pb sb and pb', sb', then la coprod lb has basis with index (i,i') and basic sets preimage unions.
Русский
Если у la и lb базисы, то их копродукс имеет базис с индексами пар и базисные множества — объединения предобразов.
LaTeX
$$HasBasis.coprod la lb with index (i,i') and basic sets preimage of sa i × union preimage sb i'.$$
Lean4
theorem coprod {ι ι' : Type*} {pa : ι → Prop} {sa : ι → Set α} {pb : ι' → Prop} {sb : ι' → Set β}
(hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
(la.coprod lb).HasBasis (fun i : ι × ι' => pa i.1 ∧ pb i.2) fun i => Prod.fst ⁻¹' sa i.1 ∪ Prod.snd ⁻¹' sb i.2 :=
(hla.comap Prod.fst).sup (hlb.comap Prod.snd)
