forall_iff_succAbove — Mathlib

English

A property P on Fin(n+1) holds for all indices iff it holds at p and for all i, P(p.succAbove i).

Русский

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

LaTeX

$$$\\\\forall i, P i \\\\iff P p \\land \\\\forall i, P(p.succAbove i)$$$

Lean4

theorem forall_iff_succAbove {P : Fin (n + 1) → Prop} (p : Fin (n + 1)) : (∀ i, P i) ↔ P p ∧ ∀ i, P (p.succAbove i) :=
  ⟨fun h ↦ ⟨h _, fun _ ↦ h _⟩, fun h ↦ succAboveCases p h.1 h.2⟩

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