English
Let r be a relation on a linear ordered archimedean pred-order with hr reflexive. If r holds from i to its successor for all i in Ico(n,m) and conversely from successor to i for all i in Ico(m,n), then there exists a finite chain from n to m using r.
Русский
Пусть r — отношение на линейном упорядоченном пред-порядке с archimedean. Если для всех i в Ico(n,m) выполняется r(i, succ i), и для всех i в Ico(m,n) выполняется r(succ i, i), а r рефлексивно, то из n можно добраться до m по цепочке из r.
LaTeX
$$\\operatorname{Reflexive}(r) \\\\wedge \\Big(\\forall i \\in \\mathrm{Ico}(n,m),\\; r(i,\\operatorname{succ} i)\\Big) \\\\wedge \\Big(\\forall i \\in \\mathrm{Ico}(m,n),\\; r(\\operatorname{succ} i,i)\\Big) \\Rightarrow \\operatorname{TransGen} r\, n\, m$$
Lean4
/-- `(n, m)` is in the transitive closure of a reflexive relation `~` if `i ~ succ i` and
`succ i ~ i` for all `i` between `n` and `m`. -/
theorem transGen_of_succ_of_reflexive (r : α → α → Prop) {n m : α} (hr : Reflexive r) (h1 : ∀ i ∈ Ico n m, r i (succ i))
(h2 : ∀ i ∈ Ico m n, r (succ i) i) : TransGen r n m :=
by
rcases eq_or_ne m n with (rfl | hmn); · exact TransGen.single (hr m)
exact transGen_of_succ_of_ne r h1 h2 hmn.symm
