mathlib docs: core.init.classical

source

axiom classical.choice {α : Sort u} :

nonempty α → α

source

theorem classical.indefinite_description {α : Sort u} (p : α → Prop) :

(∃ (x : α), p x) → {x // p x}

source

def classical.some {α : Sort u} {p : α → Prop} :

(∃ (x : α), p x) → α

Equations

classical.some h = (classical.indefinite_description p h).val

source

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

p (classical.some h)

source

theorem classical.em (p : Prop) :

p ∨ ¬p

source

theorem classical.exists_true_of_nonempty {α : Sort u} :

nonempty α → (∃ (x : α), true)

source

def classical.inhabited_of_nonempty {α : Sort u} :

nonempty α → inhabited α

Equations

classical.inhabited_of_nonempty h = {default := classical.choice h}

source

def classical.inhabited_of_exists {α : Sort u} {p : α → Prop} :

(∃ (x : α), p x) → inhabited α

Equations

classical.inhabited_of_exists h = classical.inhabited_of_nonempty _

source

def classical.prop_decidable (a : Prop) :

decidable a

Equations

classical.prop_decidable a = classical.choice _

source

def classical.decidable_inhabited (a : Prop) :

inhabited (decidable a)

Equations

classical.decidable_inhabited a = {default := classical.prop_decidable a}

source

def classical.type_decidable_eq (α : Sort u) :

decidable_eq α

Equations

classical.type_decidable_eq α = λ (x y : α), classical.prop_decidable (x = y)

source

def classical.type_decidable (α : Sort u) :

psum α (α → false)

Equations

classical.type_decidable α = classical.type_decidable._match_1 α (classical.prop_decidable (nonempty α))
classical.type_decidable._match_1 α (decidable.is_true hp) = psum.inl (inhabited.default α)
classical.type_decidable._match_1 α (decidable.is_false hn) = psum.inr _

source

theorem classical.strong_indefinite_description {α : Sort u} (p : α → Prop) :

nonempty α → {x // (∃ (y : α), p y) → p x}

source

def classical.epsilon {α : Sort u} [h : nonempty α] :

(α → Prop) → α

Equations

classical.epsilon p = (classical.strong_indefinite_description p h).val

source

theorem classical.epsilon_spec_aux {α : Sort u} (h : nonempty α) (p : α → Prop) :

(∃ (y : α), p y) → p (classical.epsilon p)

source

theorem classical.epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ (y : α), p y) :

p (classical.epsilon p)

source

theorem classical.epsilon_singleton {α : Sort u} (x : α) :

classical.epsilon (λ (y : α), y = x) = x

source

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))

source

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)

source

theorem classical.prop_complete (a : Prop) :

a = true ∨ a = false

source

def classical.eq_true_or_eq_false (a : Prop) :

a = true ∨ a = false

Equations

classical.eq_true_or_eq_false = classical.prop_complete

source

theorem classical.cases_true_false (p : Prop → Prop) (h1 : p true) (h2 : p false) (a : Prop) :

p a

source

theorem classical.cases_on (a : Prop) {p : Prop → Prop} :

p true → p false → p a

source

def classical.by_cases {p q : Prop} :

(p → q) → (¬p → q) → q

Equations

_ = _

source

theorem classical.by_contradiction {p : Prop} :

(¬p → false) → p

source

theorem classical.eq_false_or_eq_true (a : Prop) :

a = false ∨ a = true

mathlib documentation

core.init.classical

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​classical

General documentation

Additional documentation

Library

core.init.classical