# Classical reasoning support #

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

- Classical.indefiniteDescription p h = Classical.choice ⋯

Instances For

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

Given that there exists an element satisfying `p`, returns one such element.

This is a straightforward consequence of, and equivalent to, `Classical.choice`.

See also `choose_spec`, which asserts that the returned value has property `p`.

Equations

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

Instances For

source
theorem Classical.choose_spec {α : Sort u} {p : α → Prop} (h : ∃ (x : α), p x) :
p (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 }

Instances For

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 ⋯

Instances For

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

All propositions are `Decidable`.

Equations

- Classical.propDecidable a = Classical.choice ⋯

Instances For

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

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

Instances For

source
instance Classical.instNonemptyDecidable (a : Prop) :
Nonempty (Decidable a)
source
noncomputable def Classical.typeDecidableEq (α : Sort u) :
DecidableEq α
Equations

- Classical.typeDecidableEq α x✝¹ x✝ = inferInstance

Instances For

source
noncomputable def Classical.typeDecidable (α : Sort u) :
α ⊕' ∀ (a : α), False
Equations

- Classical.typeDecidable α = match Classical.propDecidable (Nonempty α) with | isTrue hp => PSum.inl default | isFalse hn => PSum.inr ⋯

Instances For

source
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.

Instances For

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

the Hilbert epsilon Function

Equations

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

Instances For

source
theorem Classical.epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : α → Prop) :
(∃ (y : α), p y) → p (epsilon p)
source
theorem Classical.epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ (y : α), p y) :
p (epsilon p)
source
theorem Classical.epsilon_singleton {α : Sort u} (x : α) :
(epsilon fun (y : α) => y = x) = x
source
theorem Classical.axiomOfChoice {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop} (h : ∀ (x : α), ∃ (y : β x), r x y) :
∃ (f : (x : α) → β x), ∀ (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 : b x), p x y) ↔ ∃ (f : (x : α) → b x), ∀ (x : α), p x (f x)
source
theorem Classical.propComplete (a : Prop) :
a = True ∨ a = False
source
theorem Classical.byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) :
q
source
theorem Classical.byContradiction {p : Prop} (h : ¬p → False) :
p
source
@[simp]
theorem Classical.not_not {a : Prop} :
¬¬a ↔ a

The Double Negation Theorem: `¬¬P` is equivalent to `P`. The left-to-right direction, double negation elimination (DNE), is classically true but not constructively.

source
def Classical.decidable_of_decidable_not (p : Prop) [h : Decidable ¬p] :
Decidable p

Transfer decidability of `¬ p` to decidability of `p`.

Equations

- Classical.decidable_of_decidable_not p = isTrue ⋯
- Classical.decidable_of_decidable_not p = isFalse h_2

Instances For

source
@[simp]
theorem Classical.dite_not {p : Prop} {α : Sort u_1} [hn : Decidable ¬p] (x : ¬p → α) (y : ¬¬p → α) :
dite (¬p) x y = dite p (fun (h : p) => y ⋯) x

Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches.

source
@[simp]
theorem Classical.ite_not {α : Sort u_1} (p : Prop) [Decidable ¬p] (x y : α) :
(if ¬p then x else y) = if p then y else x

Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches.

source
@[simp]
theorem Classical.decide_not (p : Prop) [Decidable ¬p] :
(decide ¬p) = !decide p
source
@[simp]
theorem Classical.not_forall {α : Sort u_1} {p : α → Prop} :
(¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x
source
theorem Classical.not_forall_not {α : Sort u_1} {p : α → Prop} :
(¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x
source
theorem Classical.not_exists_not {α : Sort u_1} {p : α → Prop} :
(¬∃ (x : α), ¬p x) ↔ ∀ (x : α), p x
source
theorem Classical.forall_or_exists_not {α : Sort u_1} (P : α → Prop) :
(∀ (a : α), P a) ∨ ∃ (a : α), ¬P a
source
theorem Classical.exists_or_forall_not {α : Sort u_1} (P : α → Prop) :
(∃ (a : α), P a) ∨ ∀ (a : α), ¬P a
source
theorem Classical.or_iff_not_imp_left {a b : Prop} :
a ∨ b ↔ ¬a → b
source
theorem Classical.or_iff_not_imp_right {a b : Prop} :
a ∨ b ↔ ¬b → a
source
theorem Classical.not_imp_iff_and_not {a b : Prop} :
¬(a → b) ↔ a ∧ ¬b
source
theorem Classical.not_and_iff_not_or_not {a b : Prop} :
¬(a ∧ b) ↔ ¬a ∨ ¬b
source
@[reducible, inline, deprecated Classical.not_and_iff_not_or_not (since := "2025-03-18")]
abbrev Classical.not_and_iff_or_not_not {a b : Prop} :
¬(a ∧ b) ↔ ¬a ∨ ¬b
Equations

- @Classical.not_and_iff_or_not_not = @Classical.not_and_iff_not_or_not

Instances For

source
theorem Classical.not_iff {a b : Prop} :
¬(a ↔ b) ↔ (¬a ↔ b)
source
@[simp]
theorem Classical.imp_iff_left_iff {b a : Prop} :
(b ↔ a → b) ↔ a ∨ b
source
@[simp]
theorem Classical.imp_iff_right_iff {a b : Prop} :
(a → b ↔ b) ↔ a ∨ b
source
@[simp]
theorem Classical.and_or_imp {a b c : Prop} :
a ∧ b ∨ (a → c) ↔ a → b ∨ c
source
@[simp]
theorem Classical.not_imp {a b : Prop} :
¬(a → b) ↔ a ∧ ¬b
source
@[simp]
theorem Classical.imp_and_neg_imp_iff (p : Prop) {q : Prop} :
(p → q) ∧ (¬p → q) ↔ q
source
@[reducible]
noncomputable def Exists.choose {α : Sort u_1} {p : α → Prop} (P : ∃ (a : α), p a) :
α

Extract an element from an existential statement, using `Classical.choose`.

Equations

- P.choose = Classical.choose P

Instances For

source
theorem Exists.choose_spec {α : Sort u_1} {p : α → Prop} (P : ∃ (a : α), p a) :
p P.choose

Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`.