of_cons_of_ne — Mathlib

English

If a ≠ b and a :: l1 is a sublist of b :: l2, then a :: l1 is a sublist of l2.

Русский

Если a ≠ b и a :: l1 является подпоследовательностью b :: l2, то a :: l1 является подпоследовательностью l2.

LaTeX

$$$ a \neq b \land (a :: l_1) <+ (b :: l_2) \Rightarrow (a :: l_1) <+ l_2 $$$

Lean4

/-- If the first element of two lists are different, then a sublist relation can be reduced. -/
theorem of_cons_of_ne {a b} (h₁ : a ≠ b) (h₂ : a :: l₁ <+ b :: l₂) : a :: l₁ <+ l₂ :=
  match h₁, h₂ with
  | _, .cons _ h => h

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