English
If between n and m every step through pred i relates to i in both directions, and n ≠ m, then there is a finite r-chain from n to m.
Русский
Если между n и m каждая ступень через pred i соотносится с i в обе стороны, и n ≠ m, тогда существует конечная цепочка по r от n к m.
LaTeX
$$\\forall {n,m} (r : α → α → Prop) (h1 : ∀ i ∈ \\mathrm{Ioc} m n, r i (pred i)) (h2 : ∀ i ∈ \\mathrm{Ioc} n m, r (pred i) i) (hnm : n ≠ m) : \\operatorname{TransGen} r n m$$
Lean4
/-- For `n ≠ m`, `(n, m)` is in the transitive closure of a relation `~` if `i ~ pred i` and
`pred i ~ i` for all `i` between `n` and `m`. -/
theorem transGen_of_pred_of_ne (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ioc m n, r i (pred i))
(h2 : ∀ i ∈ Ioc n m, r (pred i) i) (hnm : n ≠ m) : TransGen r n m :=
transGen_of_succ_of_ne (α := αᵒᵈ) r (fun x hx => h1 x ⟨hx.2, hx.1⟩) (fun x hx => h2 x ⟨hx.2, hx.1⟩) hnm
