English
If ι is linearly ordered and sa, sb form p-antitone bases, then (la × lb) has basis p with sa(i) × sb(i) using the opposite order.
Русский
Если ι упорядочено линейно, и sa, sb образуют антитональный базис по p, то (la × lb) имеет базис p с sa(i) × sb(i) по обратному порядку.
LaTeX
$$If ha.HasBasis p sa and hb.HasBasis p sb then (la × lb).HasBasis p (sa i × sb i) through the dual order.$$
Lean4
theorem prod_same_index_anti {ι : Type*} [LinearOrder ι] {p : ι → Prop} {sa : ι → Set α} {sb : ι → Set β}
(hla : la.HasBasis p sa) (hlb : lb.HasBasis p sb) (hsa : AntitoneOn sa {i | p i}) (hsb : AntitoneOn sb {i | p i}) :
(la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i :=
@HasBasis.prod_same_index_mono _ _ _ _ ιᵒᵈ _ _ _ _ hla hlb hsa.dual_left hsb.dual_left
