add_rev_cast — Mathlib

English

For j ∈ Fin(n+1), the sum of its value and the value of its reverse equals n: j.1 + j.rev.1 = n.

Русский

Пусть j ∈ Fin(n+1). Тогда сумма значения j и значения обратного j равна n: j.1 + j.rev.1 = n.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; j \\in \\mathrm{Fin}(n+1):\\; j.1 + j.rev.1 = n$$$

Lean4

theorem add_rev_cast (j : Fin (n + 1)) : j.1 + j.rev.1 = n :=
  by
  obtain ⟨j, hj⟩ := j
  simp [Nat.add_sub_cancel' <| le_of_lt_succ hj]

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