Init.Classical

source

noncomputable def Classical.indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ x, p x) :

{ x // p x }

Equations

Classical.indefiniteDescription p h = Classical.choice (_ : Nonempty { x // p x })

source

noncomputable def Classical.choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) :

α

Equations

Classical.choose h = (Classical.indefiniteDescription p h).val

source

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

p (Classical.choose h)

source

theorem Classical.em (p : Prop) :

p ∨ ¬p

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

source

theorem Classical.exists_true_of_nonempty {α : Sort u} :

Nonempty α → ∃ x, True

source

noncomputable def Classical.inhabited_of_nonempty {α : Sort u} (h : Nonempty α) :

Inhabited α

Equations

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

source

noncomputable def Classical.inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) :

Inhabited α

Equations

Classical.inhabited_of_exists h = Classical.inhabited_of_nonempty (_ : Nonempty α)

source

noncomputable def Classical.propDecidable (a : Prop) :

Decidable a

Equations

Classical.propDecidable a = Classical.choice (_ : Nonempty (Decidable a))

source

noncomputable def Classical.decidableInhabited (a : Prop) :

Inhabited (Decidable a)

Equations

Classical.decidableInhabited a = { default := inferInstance }

source

noncomputable def Classical.typeDecidableEq (α : Sort u) :

DecidableEq α

Equations

Classical.typeDecidableEq α x x = inferInstance

source

noncomputable def Classical.typeDecidable (α : Sort u) :

α ⊕' (α → False)

Equations

Classical.typeDecidable α = match Classical.propDecidable (Nonempty α) with | isTrue hp => PSum.inl default | isFalse hn => PSum.inr (_ : α → False)

source

noncomputable def Classical.strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : Nonempty α) :

{ x // (∃ y, p y) → p x }

Equations

Classical.strongIndefiniteDescription p h = if hp : ∃ x, p x then let_fun this := let xp := Classical.indefiniteDescription (fun x => p x) hp; { val := xp.val, property := Classical.strongIndefiniteDescription.proof_1 p hp }; this else { val := Classical.choice h, property := Classical.strongIndefiniteDescription.proof_2 p h hp }

source

noncomputable def Classical.epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) :

α

Equations

Classical.epsilon p = (Classical.strongIndefiniteDescription p h).val

the Hilbert epsilon Function

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 fun y => y = x) = x

source

theorem Classical.axiomOfChoice {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop} (h : ∀ (x : α), ∃ y, r x y) :

∃ f, (x : α) → r x (f x)

the axiom of choice

source

theorem Classical.skolem {α : Sort u} {b : α → Sort v} {p : (x : α) → b x → Prop} :

(∀ (x : α), ∃ y, p x y) ↔ ∃ f, (x : α) → p x (f x)

source

theorem Classical.propComplete (a : Prop) :

a = True ∨ a = False

source

theorem Classical.byCases {p : Prop} {q : Prop} (hpq : p → q) (hnpq : ¬p → q) :

q

source

theorem Classical.byContradiction {p : Prop} (h : ¬p → False) :

p

source

def Classical.«tacticBy_cases__:_» :

Lean.ParserDescr

Equations

Classical.«tacticBy_cases__:_» = Lean.ParserDescr.node `Classical.«tacticBy_cases__:_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "by_cases" false) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.unary `atomic (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `ident) (Lean.ParserDescr.symbol ":"))))) (Lean.ParserDescr.cat `term 0))

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.