forall_iff — Mathlib

English

If α is a type with a unique element a0, then for any predicate p: α → Prop, (for all a, p(a)) is equivalent to p(a0).

Русский

Пусть α — тип с единственным элементом a0. Тогда для любого предиката p : α → Prop верно (∀ a : α, p(a)) ⇔ p(a0).

LaTeX

$$$(\forall a:\alpha, p(a)) \iff p(a_0)$$$

Lean4

theorem forall_iff {p : α → Prop} : (∀ a, p a) ↔ p default :=
  ⟨fun h ↦ h _, fun h x ↦ by rwa [Unique.eq_default x]⟩

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