forall_fin_succ_pi — Mathlib

English

For α, P : ((i : Fin (n+1)) → α i) → Prop, we have (∀ x, P x) ↔ ∀ a v, P (Fin.cons a v).

Русский

Для α, P : ((i : Fin (n+1)) → α i) → Prop, имеем (∀ x, P x) ↔ ∀ a v, P (Fin.cons a v).

LaTeX

$$$\\forall {n} {\\alpha} {P}, \\ (\\\\forall x, P x) \\\\Leftrightarrow \\\\forall a,v, P(\\\\mathrm{Fin.cons} a v)$$$

Lean4

theorem forall_fin_succ_pi {P : (∀ i, α i) → Prop} : (∀ x, P x) ↔ ∀ a v, P (Fin.cons a v) :=
  ⟨fun h a v ↦ h (Fin.cons a v), consCases⟩

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