transGen_of_pred_of_lt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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