cons_elim — Mathlib

English

From Pairwise R (cons hd tl) derive (∀ x ∈ tl, R hd x) ∧ Pairwise R tl.

Русский

Из Pairwise R (cons hd tl) следует (∀ x ∈ tl, R hd x) ∧ Pairwise R tl.

LaTeX

$$$\text{Pairwise } R (cons\ hd\ tl) \rightarrow (∀ x \in tl, R\ hd\ x) ∧ \text{Pairwise } R\ tl$$$

Lean4

theorem cons_elim {R : α → α → Prop} {hd : α} {tl : Seq α} (h : Pairwise R (.cons hd tl)) :
    (∀ x ∈ tl, R hd x) ∧ Pairwise R tl := by
  simp only [Pairwise] at *
  refine ⟨?_, fun i j h_ij ↦ h (i + 1) (j + 1) (by omega)⟩
  intro x hx
  rw [mem_iff_exists_get?] at hx
  obtain ⟨n, hx⟩ := hx
  simpa [← hx] using h 0 (n + 1) (by omega)

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