English
If la and lb have bases with the same predicate p and sa, sb are monotone on {i | p(i)}, then (la × lb) has basis p with sa(i) × sb(i).
Русский
Если la и lb имеют базы с одинаковым предикатом p, причём sa и sb монотонны на {i | p(i)}, то (la × lb) имеет базис p с sa(i) × sb(i).
LaTeX
$$For ι with a LinearOrder, if ha.HasBasis p sa, hb.HasBasis p sb, and sa, sb are MonotoneOn on {i | p i}, then (la × lb).HasBasis p (sa i × sb i).$$
Lean4
theorem prod_same_index_mono {ι : Type*} [LinearOrder ι] {p : ι → Prop} {sa : ι → Set α} {sb : ι → Set β}
(hla : la.HasBasis p sa) (hlb : lb.HasBasis p sb) (hsa : MonotoneOn sa {i | p i}) (hsb : MonotoneOn sb {i | p i}) :
(la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i :=
hla.prod_same_index hlb fun {i j} hi hj =>
have : p (min i j) := min_rec' _ hi hj
⟨min i j, this, hsa this hi <| min_le_left _ _, hsb this hj <| min_le_right _ _⟩
