From 62c3e56247a2cd41b511bb905231baa4b6231b1a Mon Sep 17 00:00:00 2001 From: Hunter Monroe Date: Sun, 17 Dec 2023 14:10:35 -0500 Subject: [PATCH] doc: Bold "Diaconescu's theorem" (#3086) --- src/Init/Classical.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index 4d1a2772fd..db8d96db2d 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -22,7 +22,7 @@ noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α : theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) := (indefiniteDescription p h).property -/-- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/ +/-- **Diaconescu's theorem**: excluded middle from choice, Function extensionality and propositional extensionality. -/ theorem em (p : Prop) : p ∨ ¬p := let U (x : Prop) : Prop := x = True ∨ p let V (x : Prop) : Prop := x = False ∨ p