Documentation

Init.Classical

noncomputable def Classical.indefiniteDescription {α : Sort u} (p : αProp) (h : ∃ x, p x) :
{ x // p x }
Equations
noncomputable def Classical.choose {α : Sort u} {p : αProp} (h : ∃ x, p x) :
α
Equations
theorem Classical.choose_spec {α : Sort u} {p : αProp} (h : ∃ x, p x) :
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} :
Nonempty α∃ x, True
noncomputable def Classical.inhabited_of_nonempty {α : Sort u} (h : Nonempty α) :
Equations
noncomputable def Classical.inhabited_of_exists {α : Sort u} {p : αProp} (h : ∃ x, p x) :
Equations
noncomputable def Classical.propDecidable (a : Prop) :
Equations
noncomputable def Classical.decidableInhabited (a : Prop) :
Equations
noncomputable def Classical.typeDecidableEq (α : Sort u) :
Equations
noncomputable def Classical.typeDecidable (α : Sort u) :
α ⊕' (αFalse)
Equations
noncomputable def Classical.strongIndefiniteDescription {α : Sort u} (p : αProp) (h : Nonempty α) :
{ x // (∃ y, p y) → p x }
Equations
noncomputable def Classical.epsilon {α : Sort u} [h : Nonempty α] (p : αProp) :
α
Equations

the Hilbert epsilon Function

theorem Classical.epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : αProp) :
(∃ y, p y) → p (Classical.epsilon p)
theorem Classical.epsilon_spec {α : Sort u} {p : αProp} (hex : ∃ y, p y) :
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, r x y) :
∃ f, (x : α) → r x (f x)

the axiom of choice

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

by_cases(h:)?p splits the main goal into two cases, assuming h:p in the first branch, and h:¬p in the second branch.