# Classical reasoning support #

noncomputable def Classical.indefiniteDescription {α : Sort u} (p : αProp) (h : ∃ (x : α), p x) :
{ x : α // p x }
Equations
Instances For
noncomputable def Classical.choose {α : Sort u} {p : αProp} (h : ∃ (x : α), p x) :
α
Equations
• = .val
Instances For
theorem Classical.choose_spec {α : Sort u} {p : αProp} (h : ∃ (x : α), p x) :
p ()
theorem Classical.em (p : Prop) :
p ¬p

Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality.

theorem Classical.exists_true_of_nonempty {α : Sort u} :
∃ (x : α), True
noncomputable def Classical.inhabited_of_nonempty {α : Sort u} (h : ) :
Equations
• = { default := }
Instances For
noncomputable def Classical.inhabited_of_exists {α : Sort u} {p : αProp} (h : ∃ (x : α), p x) :
Equations
Instances For
noncomputable def Classical.propDecidable (a : Prop) :

All propositions are Decidable.

Equations
Instances For
noncomputable def Classical.decidableInhabited (a : Prop) :
Equations
• = { default := inferInstance }
Instances For
noncomputable def Classical.typeDecidableEq (α : Sort u) :
Equations
• = inferInstance
Instances For
noncomputable def Classical.typeDecidable (α : Sort u) :
α ⊕' (αFalse)
Equations
Instances For
noncomputable def Classical.strongIndefiniteDescription {α : Sort u} (p : αProp) (h : ) :
{ x : α // (∃ (y : α), p y)p x }
Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Classical.epsilon {α : Sort u} [h : ] (p : αProp) :
α

the Hilbert epsilon Function

Equations
Instances For
theorem Classical.epsilon_spec_aux {α : Sort u} (h : ) (p : αProp) :
(∃ (y : α), p y)p
theorem Classical.epsilon_spec {α : Sort u} {p : αProp} (hex : ∃ (y : α), p y) :
p
theorem Classical.epsilon_singleton {α : Sort u} (x : α) :
(Classical.epsilon fun (y : α) => y = x) = x
theorem Classical.axiomOfChoice {α : Sort u} {β : αSort v} {r : (x : α) → β xProp} (h : ∀ (x : α), ∃ (y : β x), r x y) :
∃ (f : (x : α) → β x), ∀ (x : α), r x (f x)

the axiom of choice

theorem Classical.skolem {α : Sort u} {b : αSort v} {p : (x : α) → b xProp} :
(∀ (x : α), ∃ (y : b x), p x y) ∃ (f : (x : α) → b x), ∀ (x : α), p x (f x)
theorem Classical.byCases {p : Prop} {q : Prop} (hpq : pq) (hnpq : ¬pq) :
q
theorem Classical.byContradiction {p : Prop} (h : ¬pFalse) :
p
theorem Classical.not_not {a : Prop} :

The Double Negation Theorem: ¬¬P is equivalent to P. The left-to-right direction, double negation elimination (DNE), is classically true but not constructively.

@[simp]
theorem Classical.not_forall {α : Sort u_1} {p : αProp} :
(¬∀ (x : α), p x) ∃ (x : α), ¬p x
theorem Classical.not_forall_not {α : Sort u_1} {p : αProp} :
(¬∀ (x : α), ¬p x) ∃ (x : α), p x
theorem Classical.not_exists_not {α : Sort u_1} {p : αProp} :
(¬∃ (x : α), ¬p x) ∀ (x : α), p x
theorem Classical.forall_or_exists_not {α : Sort u_1} (P : αProp) :
(∀ (a : α), P a) ∃ (a : α), ¬P a
theorem Classical.exists_or_forall_not {α : Sort u_1} (P : αProp) :
(∃ (a : α), P a) ∀ (a : α), ¬P a
theorem Classical.or_iff_not_imp_left {a : Prop} {b : Prop} :
a b ¬ab
theorem Classical.or_iff_not_imp_right {a : Prop} {b : Prop} :
a b ¬ba
theorem Classical.not_imp_iff_and_not {a : Prop} {b : Prop} :
¬(ab) a ¬b
theorem Classical.not_iff {a : Prop} {b : Prop} :
¬(a b) (¬a b)
@[reducible]
noncomputable def Exists.choose {α : Sort u_1} {p : αProp} (P : ∃ (a : α), p a) :
α

Extract an element from a existential statement, using Classical.choose.

Equations
Instances For
theorem Exists.choose_spec {α : Sort u_1} {p : αProp} (P : ∃ (a : α), p a) :
p ()

Show that an element extracted from P : ∃ a, p a using P.choose satisfies p.