transGen_of_succ_of_gt — Mathlib

English

If between m and n every step i → succ i satisfies r, then there is a reflexive-transitive chain from n to m whenever m ≤ n.

Русский

Если для всех i между m и n выполняется r(succ i) i, и m ≤ n, то существует рефлексивно-транзитивная цепь от n к m.

LaTeX

$$ReflTransGen r n m$$

Lean4

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

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