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) :
      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 α) :
      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
              Equations
              • =
              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 : β 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 : Prop} {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 : Prop} {b : Prop} :
                        a b ¬ab
                        theorem Classical.or_iff_not_imp_right {a : Prop} {b : Prop} :
                        a b ¬ba
                        theorem Classical.not_imp_iff_and_not {a : Prop} {b : Prop} :
                        ¬(ab) a ¬b
                        theorem Classical.not_iff {a : Prop} {b : Prop} :
                        ¬(a b) (¬a b)
                        @[simp]
                        theorem Classical.imp_iff_left_iff {b : Prop} {a : Prop} :
                        (b ab) a b
                        @[simp]
                        theorem Classical.imp_iff_right_iff {a : Prop} {b : Prop} :
                        (ab b) a b
                        @[simp]
                        theorem Classical.and_or_imp {a : Prop} {b : Prop} {c : Prop} :
                        a b (ac) ab c
                        @[simp]
                        theorem Classical.not_imp {a : Prop} {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 a 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.