mono_right — Mathlib

English

Mono_right variant: if hs holds, then Lex r s1 a b implies Lex r s2 a b.

Русский

Вариант mono_right: если hs выполняется, то Lex r s1 a b ⇒ Lex r s2 a b.

LaTeX

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

Lean4

theorem mono_right {r : ι → ι → Prop} {s₁ s₂ : ∀ i, α i → α i → Prop} (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

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