mk_eq_one — Mathlib

English

For any n,a with ha: a < n+2, the equality (⟨a, ha⟩ : Fin(n+2)) = 1 holds iff a = 1.

Русский

Пусть для любого n и a с ha: a < n+2 выполняется, что (⟨a, ha⟩ : Fin(n+2)) = 1 тогда и только тогда, когда a = 1.

LaTeX

$$$\\bigl(\\langle a, ha \\rangle : \\mathrm{Fin}(n+2)\\bigr) = 1 \\iff a = 1$$$

Lean4

@[simp]
theorem mk_eq_one {n a : Nat} {ha : a < n + 2} : (⟨a, ha⟩ : Fin (n + 2)) = 1 ↔ a = 1 :=
  mk.inj_iff

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