forall_iff — Mathlib

English

For any P, Forall P is equivalent to ∀ x, P x.

Русский

Для любого предиката P эквивалентно Forall P ↔ ∀ x, P x.

LaTeX

$$$\forall P,\; \mathrm{Forall} P \;\Leftrightarrow\; \forall x,\; P x$$$

Lean4

/-- This can be used to prove
```lean
example (P : (Fin 2 → α) → Prop) : (∀ f, P f) ↔ ∀ a₀ a₁, P ![a₀, a₁] :=
  (forall_iff _).symm
```
-/
@[simp]
theorem forall_iff : ∀ {m} (P : (Fin m → α) → Prop), Forall P ↔ ∀ x, P x
  | 0, P => by
    simp only [Forall, Fin.forall_fin_zero_pi]
    rfl
  | .succ n, P => by simp only [Forall, forall_iff, Fin.forall_fin_succ_pi, Matrix.vecCons]

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