append_left — Mathlib

English

Given a relation R, if t1 ≤ t2 holds, then for any list s, Lex R (s ++ t1) (s ++ t2) holds.

Русский

При заданной связи R, если t1 ≤ t2, то для любого списка s выполняется Lex R (s ++ t1) (s ++ t2).

LaTeX

$$$\\forall R:\\alpha\\to\\alpha\\to\\mathrm{Prop},\\forall \\{t_1,t_2\\}:\\mathrm{List}\\ \\alpha,\\ \\mathrm{Lex}\\ R\\ t_1\\ t_2 \\Rightarrow \\forall s:\\mathrm{List}\\ \\alpha,\\ \\mathrm{Lex}\\ R\\ (s++t_1)\\ (s++t_2).$$$

Lean4

theorem append_left (R : α → α → Prop) {t₁ t₂} (h : Lex R t₁ t₂) : ∀ s, Lex R (s ++ t₁) (s ++ t₂)
  | [] => h
  | _ :: l => cons (append_left R h l)

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