Classical reasoning support

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

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.

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 α

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 ⋯

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

All propositions are Decidable.

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

theorem Classical.instNonemptyDecidable (a : Prop) : Nonempty (Decidable a)

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 ⋯

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 : β x), r x y) : ∃ (f : (x : α) → β x), ∀ (x : α), r x (f x)

the axiom of choice

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)

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

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

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

@[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.

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

@[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.

@[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.

@[simp]

theorem Classical.decide_not (p : Prop) [Decidable ¬p] : (decide ¬p) = !decide p

@[simp]

theorem Classical.not_forall {α : Sort u_1} {p : α → Prop} : (¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x

theorem Classical.not_forall_not {α : Sort u_1} {p : α → Prop} : (¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x

theorem Classical.not_exists_not {α : Sort u_1} {p : α → Prop} : (¬∃ (x : α), ¬p x) ↔ ∀ (x : α), p x

theorem Classical.forall_or_exists_not {α : Sort u_1} (P : α → Prop) : (∀ (a : α), P a) ∨ ∃ (a : α), ¬P a

theorem Classical.exists_or_forall_not {α : Sort u_1} (P : α → Prop) : (∃ (a : α), P a) ∨ ∀ (a : α), ¬P a

theorem Classical.or_iff_not_imp_left {a b : Prop} : a ∨ b ↔ ¬a → b

theorem Classical.or_iff_not_imp_right {a b : Prop} : a ∨ b ↔ ¬b → a

theorem Classical.not_imp_iff_and_not {a b : Prop} : ¬(a → b) ↔ a ∧ ¬b

theorem Classical.not_and_iff_or_not_not {a b : Prop} : ¬(a ∧ b) ↔ ¬a ∨ ¬b

theorem Classical.not_iff {a b : Prop} : ¬(a ↔ b) ↔ (¬a ↔ b)

@[simp]

theorem Classical.imp_iff_left_iff {b a : Prop} : (b ↔ a → b) ↔ a ∨ b

@[simp]

theorem Classical.imp_iff_right_iff {a b : Prop} : (a → b ↔ b) ↔ a ∨ b

@[simp]

theorem Classical.and_or_imp {a b c : Prop} : a ∧ b ∨ (a → c) ↔ a → b ∨ c

@[simp]

theorem Classical.not_imp {a b : Prop} : ¬(a → b) ↔ a ∧ ¬b

@[simp]

theorem Classical.imp_and_neg_imp_iff (p : Prop) {q : Prop} : (p → q) ∧ (¬p → q) ↔ q

@[reducible]

noncomputable def Exists.choose {α : Sort u_1} {p : α → Prop} (P : ∃ (a : α), p a) : α

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

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.