English
Similarly to SumLexCongr, given RelIso's, there is a RelIso between Prod.Lex r1 r2 and Prod.Lex s1 s2.
Русский
Аналогично SumLexCongr существует RelIso между Prod.Lex r1 r2 и Prod.Lex s1 s2.
LaTeX
$$$$ \text{prodLexCongr} \; e_1\; e_2 : \mathrm{Prod.Lex}\ r_1 r_2 \cong_r \mathrm{Prod.Lex}\ s_1 s_2. $$$$
Lean4
/-- Given relation isomorphisms `r₁ ≃r s₁` and `r₂ ≃r s₂`, construct a relation isomorphism for the
lexicographic orders on the product.
-/
def prodLexCongr {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂} (e₁ : @RelIso α₁ β₁ r₁ s₁) (e₂ : @RelIso α₂ β₂ r₂ s₂) :
Prod.Lex r₁ r₂ ≃r Prod.Lex s₁ s₂ :=
⟨Equiv.prodCongr e₁.toEquiv e₂.toEquiv, by simp [Prod.lex_def, e₁.map_rel_iff, e₂.map_rel_iff, e₁.injective.eq_iff]⟩
