transGen_of_succ_of_lt — Mathlib

English

If for all i in Ico m n, r(succ i) holds and m < n, then r connects n to m through a finite chain (TransGen).

Русский

Если для всех i в Ico(m,n) верно r(succ i) и m < n, то существует трансгенеративная цепь от n к m.

LaTeX

$$TransGen r n m$$

Lean4

/-- For `n < m`, `(n, m)` is in the transitive closure of a relation `~` if `i ~ succ i`
  for all `i` between `n` and `m`. -/
theorem transGen_of_succ_of_lt (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico n m, r i (succ i)) (hnm : n < m) :
    TransGen r n m :=
  (reflTransGen_iff_eq_or_transGen.mp <| reflTransGen_of_succ_of_le r h hnm.le).resolve_left hnm.ne'

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