Add lim_le hint (#51)

lemma lim_le is in answer and tuto_lib but not in exercise hint
leanprover-community · Dec 26, 2022 · 79a6872 · 79a6872
1 parent c17f27f
commit 79a6872
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/src/exercises/09_limits_final.lean b/src/exercises/09_limits_final.lean
@@ -71,6 +71,10 @@ and their easy consequences:
 
   limit_const_sub_inv_succ (x : ℝ) : seq_limit (λ n, x - 1/(n+1)) x
 
+as well as:
+
+  lim_le (hu : seq_limit u x) (ineg : ∀ n, u n ≤ y) : x ≤ y
+
 The structure of the proof is offered. It features a new tactic: 
 `choose` which invokes the axiom of choice (observing the tactic state before and
 after using it should be enough to understand everything). 

diff --git a/src/solutions/09_limits_final.lean b/src/solutions/09_limits_final.lean
@@ -81,6 +81,10 @@ and their easy consequences:
 
   limit_const_sub_inv_succ (x : ℝ) : seq_limit (λ n, x - 1/(n+1)) x
 
+as well as:
+
+  lim_le (hu : seq_limit u x) (ineg : ∀ n, u n ≤ y) : x ≤ y
+
 The structure of the proof is offered. It features a new tactic: 
 `choose` which invokes the axiom of choice (observing the tactic state before and
 after using it should be enough to understand everything).