range_image_pred_top_sub — Mathlib

English

The image of Finset.range n under j ↦ n−1−j equals Finset.range n.

Русский

Образ Finset.range n при j ↦ n−1−j равен Finset.range n.

LaTeX

$$$\\mathrm{range}\\ n = (\\mathrm{range}\\ n).image (\\\\lambda j, n - 1 - j)$$$

Lean4

theorem range_image_pred_top_sub (n : ℕ) : ((Finset.range n).image fun j => n - 1 - j) = Finset.range n :=
  by
  cases n
  · rw [range_zero, image_empty]
  · rw [Finset.range_eq_Ico, Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)]
    simp_rw [succ_sub_succ, Nat.sub_zero, Nat.sub_self]

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