Documentation

Init.Classical

Classical reasoning support #

noncomputable def Classical.indefiniteDescription {α : Sort u} (p : αProp) (h : x, p x) :
{ x // p x }
Equations
Instances For
    noncomputable def Classical.choose {α : Sort u} {p : αProp} (h : x, p x) :
    α
    Equations
    Instances For
      theorem Classical.choose_spec {α : Sort u} {p : αProp} (h : x, p x) :
      theorem Classical.em (p : Prop) :
      p ¬p

      Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality.

      noncomputable def Classical.inhabited_of_nonempty {α : Sort u} (h : Nonempty α) :
      Equations
      Instances For
        noncomputable def Classical.inhabited_of_exists {α : Sort u} {p : αProp} (h : x, p x) :
        Equations
        Instances For
          noncomputable def Classical.propDecidable (a : Prop) :

          All propositions are Decidable.

          Equations
          Instances For
            Equations
            Instances For
              noncomputable def Classical.typeDecidableEq (α : Sort u) :
              Equations
              Instances For
                noncomputable def Classical.typeDecidable (α : Sort u) :
                α ⊕' (αFalse)
                Equations
                Instances For
                  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
                    noncomputable def Classical.epsilon {α : Sort u} [h : Nonempty α] (p : αProp) :
                    α

                    the Hilbert epsilon Function

                    Equations
                    Instances For
                      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) :
                      theorem Classical.epsilon_singleton {α : Sort u} (x : α) :
                      (Classical.epsilon fun y => y = x) = x
                      theorem Classical.axiomOfChoice {α : Sort u} {β : αSort v} {r : (x : α) → β xProp} (h : ∀ (x : α), y, r x y) :
                      f, (x : α) → r x (f x)

                      the axiom of choice

                      theorem Classical.skolem {α : Sort u} {b : αSort v} {p : (x : α) → b xProp} :
                      (∀ (x : α), y, p x y) f, (x : α) → p x (f x)
                      theorem Classical.byCases {p : Prop} {q : Prop} (hpq : pq) (hnpq : ¬pq) :
                      q
                      theorem Classical.byContradiction {p : Prop} (h : ¬pFalse) :
                      p

                      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.
                      Instances For