From 6c6a4f37b6ff7949205dbc6f7c16e86b696eb607 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Wed, 26 Feb 2025 10:20:12 +0100 Subject: [PATCH] Remove Prop annotations --- GlimpseOfLean/Exercises/Shorter.lean | 2 +- GlimpseOfLean/Introduction.lean | 4 ++-- GlimpseOfLean/Solutions/Shorter.lean | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/GlimpseOfLean/Exercises/Shorter.lean b/GlimpseOfLean/Exercises/Shorter.lean index 17f10b5..47c332f 100644 --- a/GlimpseOfLean/Exercises/Shorter.lean +++ b/GlimpseOfLean/Exercises/Shorter.lean @@ -509,7 +509,7 @@ limits of sequences of real numbers. -/ /-- A sequence `u` converges to a limit `l` if the following holds. -/ -def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε +def seq_limit (u : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε /- Let’s see an example manipulating this definition and using a lot of the tactics diff --git a/GlimpseOfLean/Introduction.lean b/GlimpseOfLean/Introduction.lean index 654754d..ecf4d8d 100644 --- a/GlimpseOfLean/Introduction.lean +++ b/GlimpseOfLean/Introduction.lean @@ -25,7 +25,7 @@ First let us review two calculus definitions. /-- A sequence `u` of real numbers converges to `l` if `∀ ε > 0, ∃ N, ∀ n ≥ N, |u_n - l| ≤ ε`. This condition will be spelled `seq_limit u l`. -/ -def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop := +def seq_limit (u : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε /- In the above definition, note that the `n`-th term of the sequence `u` is denoted @@ -41,7 +41,7 @@ may write `l ∈ ℝ` on paper. /-- A function`f : ℝ → ℝ` is continuous at `x₀` if `∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ ⇒ |f(x) - f(x₀)| ≤ ε`. This condition will be spelled `continuous_at f x₀`.-/ -def continuous_at (f : ℝ → ℝ) (x₀ : ℝ) : Prop := +def continuous_at (f : ℝ → ℝ) (x₀ : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε /-- Now we claim that if `f` is continuous at `x₀` then it is sequentially continuous diff --git a/GlimpseOfLean/Solutions/Shorter.lean b/GlimpseOfLean/Solutions/Shorter.lean index 28d695a..762cbb4 100644 --- a/GlimpseOfLean/Solutions/Shorter.lean +++ b/GlimpseOfLean/Solutions/Shorter.lean @@ -547,7 +547,7 @@ limits of sequences of real numbers. -/ /-- A sequence `u` converges to a limit `l` if the following holds. -/ -def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε +def seq_limit (u : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε /- Let’s see an example manipulating this definition and using a lot of the tactics