English
If p is a predicate on ι and ha, hb are HasBasis with p, and for all i,j with p(i), p(j) there exists k with p(k) and sa(k) ⊆ sa(i) and sb(k) ⊆ sb(j), then (la × lb) has basis p with sa(i) × sb(i).
Русский
Если p — предикат на I, ha и hb имеют базис с p, и для любых i, j с p(i), p(j) существует k с p(k) и sa(k) ⊆ sa(i), sb(k) ⊆ sb(j), тогда (la × lb) имеет базис p с sa(i) × sb(i).
LaTeX
$$$\text{If } ha: la.HasBasis p sa,\; hb: lb.HasBasis p sb,\; (\forall i,j\, (p i)\land(p j) \Rightarrow \exists k, (p k) \land sa(k) \subseteq sa(i) \land sb(k) \subseteq sb(j))\text{ then } (la \times lb).HasBasis p (\lambda i, sa(i) \times sb(i)).$$$
Lean4
theorem prod_same_index {p : ι → Prop} {sb : ι → Set β} (hla : la.HasBasis p sa) (hlb : lb.HasBasis p sb)
(h_dir : ∀ {i j}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j) : (la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i :=
by
simp only [hasBasis_iff, (hla.prod_pprod hlb).mem_iff]
refine fun t => ⟨?_, ?_⟩
· rintro ⟨⟨i, j⟩, ⟨hi, hj⟩, hsub : sa i ×ˢ sb j ⊆ t⟩
rcases h_dir hi hj with ⟨k, hk, ki, kj⟩
exact ⟨k, hk, (Set.prod_mono ki kj).trans hsub⟩
· rintro ⟨i, hi, h⟩
exact ⟨⟨i, i⟩, ⟨hi, hi⟩, h⟩
