Init.Classical

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.epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) :

the Hilbert epsilon Function

Equations

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

source

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

source

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.