mono_left — Mathlib

English

Mono_left variant: if hr holds, then Lex r2 s a b follows from Lex r1 s a b.

Русский

Вариант mono_left: если hr выполняется, то Lex r2 s a b следует из Lex r1 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 {r₁ r₂ : ι → ι → Prop} {s : ∀ i, α i → α i → Prop} (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

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