forall_iff_castSucc — Mathlib

English

A property P on Fin(n+1) holds for all indices iff it holds for last and all i.castSucc.

Русский

Свойство P на Fin(n+1) выполняется для всех индексов тогда и только тогда, когда оно выполняется для последнего элемента и для всех i.castSucc.

LaTeX

$$$\\\\forall P : Fin(n+1) \\to Prop, \\\\bigl( (\\\\forall i, P i) \\iff (P(\\\\mathrm{last} n) \\\\wedge \\\\forall i: Fin n, P(i \\\\mathrm{castSucc})) \\bigr)$$$

Lean4

theorem forall_iff_castSucc {P : Fin (n + 1) → Prop} : (∀ i, P i) ↔ P (last n) ∧ ∀ i : Fin n, P i.castSucc :=
  ⟨fun h ↦ ⟨h _, fun _ ↦ h _⟩, fun h ↦ lastCases h.1 h.2⟩

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