proposition: Theorem squeeze_theorem : ∀ (a : ℕ → ℝ) (b : ℕ → ℝ) (c : ℕ → ℝ) (l : ℝ), (∀ n : ℕ, a n ≤ b n ∧ b n ≤ c n) ⇒ a ⟶ l ⇒ c ⟶ l ⇒ b ⟶ l.
proof: Proof. Take a, b, c : (ℕ ⇨ ℝ) and l : ℝ. Assume that (∀ n : ℕ, a n ≤ b n ∧ b n ≤ c n) and (a ⟶ l). Assume that (c ⟶ l). To show: (∀ ε : ℝ, ε > 0 ⇒ ∃ N : ℕ, ∀ n : ℕ, (n ≥ N)%nat ⇒ |b n - l| < ε). Take ε : ℝ; such that (ε > 0). It holds that (∃ N : ℕ, ∀ n : ℕ, (n ≥ N)%nat ⇒ |a n - l| < ε). Obtain such an Na. It holds that (∃ N : ℕ, ∀ n : ℕ, (n ≥ N)%nat ⇒ |c n - l| < ε). Obtain such an Nc. Choose Nn := (Nat.max Na Nc). Take n : ℕ; such that (n ≥ Nn)%nat. We claim that (-ε < a n - l). { It holds that (n ≥ Na)%nat. It holds that (R_dist (a n) l < ε) (iii). By Rabs_def2 it holds that (a n - l < ε /\ -ε < a n - l). We conclude that (-ε < a n - l). } We claim that (c n - l < ε). { It holds that (n ≥ Nc)%nat. It holds that (R_dist (c n) l < ε) (iii). By Rabs_def2 it holds that (c n - l < ε /\ -ε < c n - l). We conclude that (c n - l < ε). } It suffices to show that (-ε < b n - l < ε). It holds that (a n ≤ b n ∧ b n ≤ c n). We show both (- ε < b n - l) and ( b n - l < ε). - We conclude that (& - ε < a n - l <= b n - l). - We conclude that (& b n - l <= c n - l < ε). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Tactics Automation Libs.Reals Notations