mathlib documentation

core.init.classical

axiom classical.choice {α : Sort u} :
nonempty α → α

theorem classical.indefinite_description {α : Sort u} (p : α → Prop) :
(∃ (x : α), p x){x // p x}

def classical.some {α : Sort u} {p : α → Prop} :
(∃ (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)

def classical.inhabited_of_exists {α : Sort u} {p : α → Prop} :
(∃ (x : α), p x)inhabited α

Equations
def classical.type_decidable_eq (α : Sort u) :

Equations
def classical.type_decidable (α : Sort u) :
psum α (α → false)

Equations
theorem classical.strong_indefinite_description {α : Sort u} (p : α → Prop) :
nonempty α{x // (∃ (y : α), p y)p x}

def classical.epsilon {α : Sort u} [h : nonempty α] :
(α → Prop) → α

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} :
(∀ (x : α), ∃ (y : β x), r x y)(∃ (f : Π (x : α), β x), ∀ (x : α), r x (f x))

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} :
p truep falsep a

def classical.by_cases {p q : Prop} :
(p → q)(¬p → q) → q

theorem classical.by_contradiction {p : Prop} :
(¬p → false) → p

theorem classical.eq_false_or_eq_true (a : Prop) :