reflTransGen_of_succ_of_le — Mathlib

English

The map toZ is order-reflecting: if toZ i ≤ toZ j, then i ≤ j.

Русский

Отображение toZ отражает порядок: если toZ i ≤ toZ j, то i ≤ j.

LaTeX

$$toZ(i_0,i) \le toZ(i_0,j) \implies i \le j$$

Lean4

/-- For `n ≤ m`, `(n, m)` is in the reflexive-transitive closure of `~` if `i ~ succ i`
  for all `i` between `n` and `m`. -/
theorem reflTransGen_of_succ_of_le (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico n m, r i (succ i)) (hnm : n ≤ m) :
    ReflTransGen r n m := by
  revert h; refine Succ.rec ?_ ?_ hnm
  · intro _
    exact ReflTransGen.refl
  · intro m hnm ih h
    have : ReflTransGen r n m := ih fun i hi => h i ⟨hi.1, hi.2.trans_le <| le_succ m⟩
    rcases (le_succ m).eq_or_lt with hm | hm
    · rwa [← hm]
    exact this.tail (h m ⟨hnm, hm⟩)

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