mono_left — Mathlib

English

If hr: ∀a,b, r1 a b → r2 a b, then Lex r1 s a b → Lex r2 s a b.

Русский

Если hr: ∀a,b, r1 a b → r2 a b, то Lex r1 s a b → Lex r2 s a b.

LaTeX

$$$\\text{mono\\_left}:\\; \\forall \\{a,b\\},\\; r_1 a b \\to r_2 a b \\Rightarrow (\\operatorname{Lex} r_1 s a b) \\to (\\operatorname{Lex} r_2 s a b).$$$

Lean4

theorem mono_left (hr : ∀ a b, r₁ a b → r₂ a b) {a b : Σ i, α i} (h : Lex r₁ s a b) : Lex r₂ s a b :=
  h.mono hr fun _ _ _ => id

Похожие утверждения