English
Let α be a type, p a predicate on α, b a proposition. Then (∀ x, p x) → b is equivalent to ∃ x, p x → b, provided α is nonempty.
Русский
Пусть α — множество, p — предикат над α, b — proposition. Тогда (∀ x, p x) → b эквивалентно ∃ x, p x → b при непустом α.
LaTeX
$$$${\\forall x, p(x) \\to b} \\quad\\Longleftrightarrow\\quad {\\exists x, p(x) \\to b}$$$$
Lean4
theorem forall_imp_iff_exists_imp {α : Sort*} {p : α → Prop} {b : Prop} [ha : Nonempty α] :
(∀ x, p x) → b ↔ ∃ x, p x → b := by
classical
let ⟨a⟩ := ha
refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (_root_.not_imp.1 (h' x)).1
