English
Mono lemma: if hr and hs hold, then Lex r2 s2 on PSigma follows from Lex r1 s1 on PSigma.
Русский
Лемма монотонности: если выполняются hr и hs, то Lex r2 s2 на PSigma следует из Lex r1 s1 на PSigma.
LaTeX
$$$\\text{mono}:\\; (hr: \\forall a b, r_1 a b \\to r_2 a b) \\to (hs: \\forall i a b, s_1 i a b \\to s_2 i a b) \\to \\forall {a b : \\Sigma' i, \\alpha i}, \\mathrm{Lex}\\ r_1 s_1\\ a\\ b \\to \\mathrm{Lex}\\ r_2 s_2\\ a\\ b.$$$
Lean4
theorem mono {r₁ r₂ : ι → ι → Prop} {s₁ s₂ : ∀ i, α i → α i → Prop} (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⟩ | ⟨i, hab⟩ := h
· exact Lex.left _ _ (hr _ _ hij)
· exact Lex.right _ (hs _ _ _ hab)
