English
Lex r s a b is equivalent to Lex with swapped coordinates: Lex (Function.swap r) s a b ↔ Lex r (i ↦ Function.swap(s i)) b a.
Русский
Lex r s a b эквивалентно Lex с обменом координат: Lex (Function.swap r) s a b ↔ Lex r (i ↦ Function.swap(s i)) b a.
LaTeX
$$$\\operatorname{lex\\_swap}:\\; \\operatorname{Lex}(\\operatorname{Function.swap} r) s\, a\, b \\;\\leftrightarrow\\; \\operatorname{Lex} r (\\lambda i. \\operatorname{Function.swap}(s i))\, b\, a$$$
Lean4
theorem lex_swap : Lex (Function.swap r) s a b ↔ Lex r (fun i => Function.swap (s i)) b a := by
constructor <;>
· rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
· exact Lex.left _ _ h
· exact Lex.right _ _ h
