Documentation

Mathlib.Init.Classical

alignments from lean 3 init.classical #

theorem Classical.axiom_of_choice {α : Sort u} {β : αSort v} {r : (x : α) → β xProp} (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.cases_true_false (p : PropProp) (h1 : p True) (h2 : p False) (a : Prop) :
p a
theorem Classical.cases_on (a : Prop) {p : PropProp} (h1 : p True) (h2 : p False) :
p a
theorem Classical.cases {p : PropProp} (h1 : p True) (h2 : p False) (a : Prop) :
p a
theorem Classical.by_cases {p : Prop} {q : Prop} (hpq : pq) (hnpq : ¬pq) :
q

Alias of Classical.byCases.