mono_right — Mathlib

English

If hs: ∀i a b, s1 i a b → s2 i a b, then Lex r s1 a b → Lex r s2 a b.

Русский

Если hs: ∀i a b, s1 i a b → s2 i a b, то Lex r s1 a b → Lex r s2 a b.

LaTeX

$$$\\text{mono\\_right}:\\; \\forall i,a,b, s_1 i a b \\to s_2 i a b \\Rightarrow (\\operatorname{Lex} r s_1 a b) \\to (\\operatorname{Lex} r s_2 a b).$$$

Lean4

theorem mono_right (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 :=
  h.mono (fun _ _ => id) hs

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