English
For p, q and a connecting edge, the i-th element at the right side of (p ⧺ q) equals q i for i in the right range.
Русский
Для p, q и соединения, i-й элемент справа в (p ⧺ q) равен q i на правой части.
LaTeX
$$$ (p \\append q \\;\\text{connect}).toFun (q.length + i) = q_{i} $$$
Lean4
/-- A relation series `a₀ -r→ a₁ -r→ ... -r→ aₙ` of `r` gives a relation series of the reverse of `r`
by reversing the series `aₙ ←r- aₙ₋₁ ←r- ... ←r- a₁ ←r- a₀`.
-/
@[simps length]
def reverse (p : RelSeries r) : RelSeries r.inv
where
length := p.length
toFun := p ∘ Fin.rev
step
i := by
rw [Function.comp_apply, Function.comp_apply, SetRel.mem_inv]
have hi : i.1 + 1 ≤ p.length := by omega
convert p.step ⟨p.length - (i.1 + 1), Nat.sub_lt_self (by omega) hi⟩
· ext; simp
· ext
simp only [Fin.val_rev, Fin.coe_castSucc, Fin.val_succ]
omega
