English
If r is reflexive and r(i, pred i) for i in Ioc m n and r(pred i, i) for i in Ioc n m, then there is a TransGen from n to m.
Русский
Если r рефлексивно и выполняется r(i, pred i) для i в Ioc(m,n) и r(pred i, i) для i в Ioc(n,m), то существует TransGen от n к m.
LaTeX
$$\\operatorname{Reflexive}(r) \\\\wedge \\Big(\\forall i \\in \\mathrm{Ioc}(m,n),\\; r(i, \\mathrm{pred}\\, i)\\Big) \\\\wedge \\Big(\\forall i \\in \\mathrm{Ioc}(n,m),\\; r(\\mathrm{pred}\\, i, i)\\Big) \\\\Rightarrow \\operatorname{TransGen} r n m$$
Lean4
/-- `(n, m)` is in the transitive closure of a reflexive relation `~` if `i ~ pred i` and
`pred i ~ i` for all `i` between `n` and `m`. -/
theorem transGen_of_pred_of_reflexive (r : α → α → Prop) {n m : α} (hr : Reflexive r) (h1 : ∀ i ∈ Ioc m n, r i (pred i))
(h2 : ∀ i ∈ Ioc n m, r (pred i) i) : TransGen r n m :=
transGen_of_succ_of_reflexive (α := αᵒᵈ) r hr (fun x hx => h1 x ⟨hx.2, hx.1⟩) fun x hx => h2 x ⟨hx.2, hx.1⟩
