Documentation

Analysis.Appendix_A_5

Analysis I, Appendix A.5: Nested quantifiers #

Some examples of nested quantifiers in Lean

source
theorem square_expand (x : ℝ) :
(x + 1) ^ 2 = x ^ 2 + 2 * x + 1
source
theorem solve_quadratic :
∃ (x : ℝ), x ^ 2 + 2 * x - 8 = 0
source
def Exercise_A_5_1a :
Decidable (∀ x > 0, ∀ y > 0, y ^ 2 = x)

Exercise A.5.1

Equations
Instances For
    source
    def Exercise_A_5_1b :
    Decidable (∃ x > 0, ∀ y > 0, y ^ 2 = x)
    Equations
    Instances For
      source
      def Exercise_A_5_1c :
      Decidable (∃ x > 0, ∃ y > 0, y ^ 2 = x)
      Equations
      Instances For
        source
        def Exercise_A_5_1d :
        Decidable (∀ y > 0, ∃ x > 0, y ^ 2 = x)
        Equations
        Instances For
          source
          def Exercise_A_5_1e :
          Decidable (∃ y > 0, ∀ x > 0, y ^ 2 = x)
          Equations
          Instances For