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) :
      α

      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
        Instances For
          theorem Classical.choose_spec {α : Sort u} {p : αProp} (h : (x : α), p x) :
          p (choose h)
          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) :
                              α ⊕' ∀ (a : α), False
                              Equations
                                Instances For
                                  noncomputable def Classical.strongIndefiniteDescription {α : Sort u} (p : αProp) (h : Nonempty α) :
                                  { x : α // ( (y : α), p y) → p x }
                                  Equations
                                    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 (epsilon p)
                                          theorem Classical.epsilon_spec {α : Sort u} {p : αProp} (hex : (y : α), p y) :
                                          p (epsilon p)
                                          theorem Classical.epsilon_singleton {α : Sort u} (x : α) :
                                          (epsilon fun (y : α) => y = x) = x
                                          theorem Classical.axiomOfChoice {α : Sort u} {β : αSort v} {r : (x : α) → β xProp} (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 xProp} :
                                          (∀ (x : α), (y : b x), p x y) (f : (x : α) → b x), ∀ (x : α), p x (f x)
                                          theorem Classical.byCases {p q : Prop} (hpq : pq) (hnpq : ¬pq) :
                                          q
                                          theorem Classical.byContradiction {p : Prop} (h : ¬pFalse) :
                                          p
                                          @[simp]
                                          theorem Classical.not_not {a : Prop} :

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

                                          Transfer decidability of ¬ p to decidability of p.

                                          Equations
                                            Instances For
                                              @[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]
                                              @[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 ¬ab
                                              theorem Classical.or_iff_not_imp_right {a b : Prop} :
                                              a b ¬ba
                                              theorem Classical.not_imp_iff_and_not {a b : Prop} :
                                              ¬(ab) a ¬b
                                              @[reducible, inline, deprecated Classical.not_and_iff_not_or_not (since := "2025-03-18")]
                                              Equations
                                                Instances For
                                                  theorem Classical.not_iff {a b : Prop} :
                                                  ¬(a b) (¬a b)
                                                  @[simp]
                                                  theorem Classical.imp_iff_left_iff {b a : Prop} :
                                                  (b ab) a b
                                                  @[simp]
                                                  theorem Classical.imp_iff_right_iff {a b : Prop} :
                                                  (ab b) a b
                                                  @[simp]
                                                  theorem Classical.and_or_imp {a b c : Prop} :
                                                  a b (ac) ab c
                                                  @[simp]
                                                  theorem Classical.not_imp {a b : Prop} :
                                                  ¬(ab) a ¬b
                                                  @[simp]
                                                  theorem Classical.imp_and_neg_imp_iff (p : Prop) {q : Prop} :
                                                  (pq) (¬pq) q
                                                  @[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
                                                    Instances For
                                                      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.