exists_not_getElem_of_not_isChain

English

If a list is not an R-chain, there exists an index n such that the n-th element and the next element are not related by R.

Русский

Если список не образует цепь по отношению R, существует индекс n, для которого элементы на позициях n и n+1 не связаны отношением R.

LaTeX

$$$\\forall {l:{\\it List }\\,\\alpha}, \\, \\neg IsChain\\, R\\, l \\Rightarrow \\exists n:\\mathbb{N}, \\exists h:\\ n+1 < l.length, \\neg R\\ (l[n]) (l[n+1])$$$

Lean4

theorem exists_not_getElem_of_not_isChain (h : ¬List.IsChain R l) : ∃ n : ℕ, ∃ h : n + 1 < l.length, ¬R l[n] l[n + 1] :=
  by simp_all [isChain_iff_getElem]

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