reflTransGen_of_succ_of_ge — Mathlib

English

With NoMaxOrder, toZ i0 (succ^[n] i0) = n for all n.

Русский

При NoMaxOrder: toZ i0 (succ^[n] i0) = n для всех n.

LaTeX

$$toZ(i_0, Nat.iterate(Order.succ, n, i_0)) = n$$

Lean4

/-- For `m ≤ n`, `(n, m)` is in the reflexive-transitive closure of `~` if `succ i ~ i`
  for all `i` between `n` and `m`. -/
theorem reflTransGen_of_succ_of_ge (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico m n, r (succ i) i) (hmn : m ≤ n) :
    ReflTransGen r n m := by
  rw [← reflTransGen_swap]
  exact reflTransGen_of_succ_of_le (swap r) h hmn

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