English
If for all i in Ioc n m, r (pred i) i and n ≤ m, then there is a reflexive-transitive chain from n to m.
Русский
Если для всех i в Ioc(n,m) выполняется r(pred i, i) и n ≤ m, то существует рефлексивно-транзитивная цепочка от n к m.
LaTeX
$$\\forall i \\in \\mathrm{Ioc}(n,m),\\; r(\\mathrm{pred}\\, i,i) \\quad\\land\\quad n \\le m \\\n\\Rightarrow\\; \\operatorname{ReflTransGen} r\\ n\\ m$$
Lean4
/-- For `n ≤ m`, `(n, m)` is in the reflexive-transitive closure of `~` if `pred i ~ i`
for all `i` between `n` and `m`. -/
theorem reflTransGen_of_pred_of_le (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc n m, r (pred i) i) (hmn : n ≤ m) :
ReflTransGen r n m :=
reflTransGen_of_succ_of_ge (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hmn
