hlast' — Mathlib

English

For i and τ with 1 ≤ τ, we have a.r(last N) ≤ τ · a.r(i).

Русский

Для i и τ с 1 ≤ τ выполняется a.r(last N) ≤ τ · a.r(i).

LaTeX

$$∀ i, 1 ≤ τ → a.r (last N) ≤ τ · a.r i$$

Lean4

theorem hlast' (i : Fin N.succ) (h : 1 ≤ τ) : a.r (last N) ≤ τ * a.r i :=
  by
  rcases lt_or_ge i (last N) with (H | H)
  · exact (a.hlast i H).2
  · have : i = last N := top_le_iff.1 H
    rw [this]
    exact le_mul_of_one_le_left (a.rpos _).le h

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