English
If r1→r2 and s1→s2 push forward under hr and hs respectively, then Lex r1 s1 a b implies Lex r2 s2 a b.
Русский
Если r1 удовлетворяет переходу в r2 и s1 переходу в s2 под отображениями hr, hs соответственно, то Lex r1 s1 a b следует из Lex r2 s2 a b.
LaTeX
$$$\\text{mono}\\;: \\forall a,b, r_1 a b \\to r_2 a b,\\; \\forall i,a,b, s_1 i a b \\to s_2 i a b,\\; {a,b}:\\Sigma i,\\alpha i,\\; \\operatorname{Lex} r_1 s_1 a b \\to \\operatorname{Lex} r_2 s_2 a b.$$$
Lean4
theorem mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ i, α i} (h : Lex r₁ s₁ a b) :
Lex r₂ s₂ a b := by
obtain ⟨a, b, hij⟩ | ⟨a, b, hab⟩ := h
· exact Lex.left _ _ (hr _ _ hij)
· exact Lex.right _ _ (hs _ _ _ hab)
