append — Mathlib

English

If l1 and l2 are IsChain R and every cross-pair (last of l1, first of l2) satisfies R, then their concatenation l1 ++ l2 is an IsChain R.

Русский

Если l1 и l2 — IsChain R и каждая пара кросса (последний элемент l1, первый элемент l2) удовлетворяет R, то их конкатенация является IsChain R.

LaTeX

$$IsChain R l1 → IsChain R l2 → (∀ x ∈ l1.getLast?, ∀ y ∈ l2.head?, R x y) → IsChain R (l1 ++ l2)$$

Lean4

theorem append (h₁ : IsChain R l₁) (h₂ : IsChain R l₂) (h : ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y) :
    IsChain R (l₁ ++ l₂) :=
  isChain_append.2 ⟨h₁, h₂, h⟩

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