Classical reasoning support

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

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

Equations

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

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

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 α) : Inhabited α

Equations

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

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

noncomputable def Classical.propDecidable (a : Prop) : Decidable a

All propositions are Decidable.

Equations

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

noncomputable def Classical.decidableInhabited (a : Prop) : Inhabited (Decidable a)

Equations

• Classical.decidableInhabited a = { default := inferInstance }

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

Equations

• Classical.typeDecidableEq α x x = inferInstance

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)

noncomputable def Classical.strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : Nonempty α) : { x // (∃ y, p y) → p x }

Equations

• One or more equations did not get rendered due to their size.

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

the Hilbert epsilon Function

Equations

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

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) : p (Classical.epsilon p)

theorem Classical.epsilon_singleton {α : Sort u} (x : α) : (Classical.epsilon fun y => y = x) = x

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

theorem Classical.skolem {α : Sort u} {b : α → Sort v} {p : (x : α) → b x → Prop} : (∀ (x : α), ∃ y, p x y) ↔ ∃ f, (x : α) → p x (f x)

theorem Classical.propComplete (a : Prop) : a = True ∨ a = False

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

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

def Classical.«tacticBy_cases_:_» : Lean.ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.