transGen_of_pred_of_gt — Mathlib

English

For i in Ioc m n, if r i (pred i) and m < n, then there is a finite r-chain from n to m.

Русский

Для i в Ioc(m,n), если r i (pred i) и m < n, тогда существует конечная цепочка по r от n к m.

LaTeX

$$\\forall i \\in \\mathrm{Ioc}(m,n),\\; r(i,\\mathrm{pred}\\, i) \\Rightarrow \\operatorname{TransGen} r\\ n\\ m$$

Lean4

/-- For `m < n`, `(n, m)` is in the transitive closure of a relation `~` for `n ≠ m` if `i ~ pred i`
  for all `i` between `n` and `m`. -/
theorem transGen_of_pred_of_gt (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc m n, r i (pred i)) (hnm : m < n) :
    TransGen r n m :=
  transGen_of_succ_of_lt (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hnm

Похожие утверждения