alignments from lean 3 init.classical

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

Alias of Classical.axiomOfChoice.

---

the axiom of choice

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

Alias of Classical.propComplete.

theorem Classical.cases_true_false (p : Prop → Prop) (h1 : p True) (h2 : p False) (a : Prop) : p a

theorem Classical.cases_on (a : Prop) {p : Prop → Prop} (h1 : p True) (h2 : p False) : p a

theorem Classical.cases {p : Prop → Prop} (h1 : p True) (h2 : p False) (a : Prop) : p a

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

Alias of Classical.byCases.

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

Alias of Classical.byContradiction.

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