English
If r relates each i to its predecessor on an interval and its predecessor relates back on the reverse interval, then there is a reflexive-transitive chain from n to m.
Русский
Если r связывает каждое i с предшественником на промежутке и предшественник связывает обратно на обратном промежутке, то существует рефлексивно-транзитивная цепочка от n к m.
LaTeX
$$\\forall i \\in \\mathrm{Ioc}(m,n),\\; r(i, \\mathrm{pred}\\, i) \\quad\\land\\quad \\forall i \\in \\mathrm{Ioc}(n,m),\\; r(\\mathrm{pred}\\, i, i) \\\\Rightarrow \\\\operatorname{ReflTransGen} r\\ n\\ m$$
Lean4
/-- `(n, m)` is in the reflexive-transitive closure of `~` if `i ~ pred i` and `pred i ~ i`
for all `i` between `n` and `m`. -/
theorem reflTransGen_of_pred (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ioc m n, r i (pred i))
(h2 : ∀ i ∈ Ioc n m, r (pred i) i) : ReflTransGen r n m :=
reflTransGen_of_succ (α := αᵒᵈ) r (fun x hx => h1 x ⟨hx.2, hx.1⟩) fun x hx => h2 x ⟨hx.2, hx.1⟩
