mathlib3 documentation

core / init.classical

axiom classical.choice {α : Sort u} :

The axiom

@[irreducible]
noncomputable def classical.indefinite_description {α : Sort u} (p : α Prop) (h : (x : α), p x) :
{x // p x}
Equations
noncomputable def classical.some {α : Sort u} {p : α Prop} (h : (x : α), p x) :
α
Equations
theorem classical.some_spec {α : Sort u} {p : α Prop} (h : (x : α), p x) :
theorem classical.em (p : Prop) :
p ¬p
theorem classical.exists_true_of_nonempty {α : Sort u} :
nonempty α ( (x : α), true)
noncomputable def classical.inhabited_of_exists {α : Sort u} {p : α Prop} (h : (x : α), p x) :
Equations
noncomputable def classical.prop_decidable (a : Prop) :

All propositions are decidable

Equations
noncomputable def classical.type_decidable_eq (α : Sort u) :
Equations
noncomputable def classical.type_decidable (α : Sort u) :
psum α false)
Equations
@[irreducible]
noncomputable def classical.strong_indefinite_description {α : Sort u} (p : α Prop) (h : nonempty α) :
{x // ( (y : α), p y) p x}
Equations
noncomputable def classical.epsilon {α : Sort u} [h : nonempty α] (p : α Prop) :
α

The Hilbert epsilon function

Equations
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 (λ (y : α), y = x) = x
theorem classical.axiom_of_choice {α : Sort u} {β : α Sort v} {r : Π (x : α), β x Prop} (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 x Prop} :
( (x : α), (y : b x), p x y) (f : Π (x : α), b x), (x : α), p x (f x)
theorem classical.prop_complete (a : Prop) :
theorem classical.cases_true_false (p : Prop Prop) (h1 : p true) (h2 : p false) (a : Prop) :
p a
theorem classical.cases_on (a : Prop) {p : Prop Prop} (h1 : p true) (h2 : p false) :
p a
theorem classical.by_cases {p q : Prop} (hpq : p q) (hnpq : ¬p q) :
q
theorem classical.by_contradiction {p : Prop} (h : ¬p false) :
p
theorem classical.eq_false_or_eq_true (a : Prop) :