forall — Mathlib

English

Let α be a type. For any predicate p on Nonempty α, (∀ h : Nonempty α, p h) is equivalent to ∀ a, p ⟨a⟩.

Русский

Пусть α — тип. Для любого предиката p на Nonempty α, (∀ h : Nonempty α, p h) эквивалентно ∀ a, p ⟨a⟩.

LaTeX

$$$ \forall {\alpha}, \forall {p : Nonempty(\alpha) \to \mathrm{Prop}}, \big( \forall h : Nonempty(\alpha), p(h) \big) \iff \forall a, p(\langle a \rangle) $$$

Lean4

@[simp]
theorem «forall» {α} {p : Nonempty α → Prop} : (∀ h : Nonempty α, p h) ↔ ∀ a, p ⟨a⟩ :=
  Iff.intro (fun h _ ↦ h _) fun h ⟨a⟩ ↦ h a

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