sizeUpTo_index_le — Mathlib

English

For any j ∈ Fin n, the natural-valued inequality c.sizeUpTo(index j) ≤ j holds.

Русский

Для любого j ∈ Fin n выполняется c.sizeUpTo(index j) ≤ j.

LaTeX

$$$ c.sizeUpTo (c.index j) \\le j $$$

Lean4

theorem sizeUpTo_index_le (j : Fin n) : c.sizeUpTo (c.index j) ≤ j :=
  by
  by_contra H
  set i := c.index j
  push_neg at H
  have i_pos : (0 : ℕ) < i := by
    by_contra! i_pos
    revert H
    simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]
  let i₁ := (i : ℕ).pred
  have i₁_lt_i : i₁ < i := Nat.pred_lt (ne_of_gt i_pos)
  have i₁_succ : i₁ + 1 = i := Nat.succ_pred_eq_of_pos i_pos
  have := Nat.find_min (c.index_exists j.2) i₁_lt_i
  simp_all [lt_trans i₁_lt_i (c.index j).2]

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