English
If p and q are r-series with a linking relation between p.last and q.head, then there exists a joined r-series of length length(p) + length(q) + 1, whose elements are obtained by concatenating p and q with the joining element in between.
Русский
Если p и q — r-ряды и между p.last и q.head существует связь по отношению r, то существует объединённый r-ряд длины length(p) + length(q) + 1, состоящий из элементов p, затем соединительный элемент, затем элементы q.
LaTeX
$$$ \\exists (p \\append q) \\;\\text{with } \\operatorname{length}(p \\append q) = p.\\text{length} + q.\\text{length} + 1 \\,\\text{and}\\; \\operatorname{toFun}(p \\append q) = \\text{(concatenation of the sequences)} $$$
Lean4
/-- If `a₀ -r→ a₁ -r→ ... -r→ aₙ` and `b₀ -r→ b₁ -r→ ... -r→ bₘ` are two strict series
such that `r aₙ b₀`, then there is a chain of length `n + m + 1` given by
`a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ b₀ -r→ b₁ -r→ ... -r→ bₘ`.
-/
@[simps length]
def append (p q : RelSeries r) (connect : p.last ~[r] q.head) : RelSeries r
where
length := p.length + q.length + 1
toFun := Fin.append p q ∘ Fin.cast (by omega)
step
i := by
obtain hi | rfl | hi := lt_trichotomy i (Fin.castLE (by omega) (Fin.last _ : Fin (p.length + 1)))
· convert p.step ⟨i.1, hi⟩ <;> convert Fin.append_left p q _ <;> rfl
· convert connect
· convert Fin.append_left p q _
· convert Fin.append_right p q _; rfl
· set x := _; set y := _
change Fin.append p q x ~[r] Fin.append p q y
have hx : x = Fin.natAdd _ ⟨i - (p.length + 1), Nat.sub_lt_left_of_lt_add hi <| i.2.trans <| by omega⟩ := by ext;
dsimp [x, y]; rw [Nat.add_sub_cancel']; exact hi
have hy : y = Fin.natAdd _ ⟨i - p.length, Nat.sub_lt_left_of_lt_add (le_of_lt hi) (by exact i.2)⟩ :=
by
ext
dsimp
conv_rhs =>
rw [Nat.add_comm p.length 1, add_assoc, Nat.add_sub_cancel' <| le_of_lt (show p.length < i.1 from hi),
add_comm]
rfl
rw [hx, Fin.append_right, hy, Fin.append_right]
convert q.step ⟨i - (p.length + 1), Nat.sub_lt_left_of_lt_add hi <| by omega⟩
rw [Fin.succ_mk, Nat.sub_eq_iff_eq_add (le_of_lt hi : p.length ≤ i), Nat.add_assoc _ 1, add_comm 1,
Nat.sub_add_cancel]
exact hi
