# The sandwich theorem

In this demo file, we define limits of sequences of real numbers and prove the sandwich theorem.

Definition
A sequence of real numbers $a_n$ tends to $l$ if $\forall \varepsilon > 0, \exists N, \forall n \geq N, |a_n - l | \leq \varepsilon$.
definition is_limit (a : ℕ → ℝ) (l : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, | a n - l | < ε

Theorem

If $(a_n)$, $(b_n)$, and $(c_n)$ are three real-valued sequences satisfying $a_n ≤ b_n ≤ c_n$ for all $n$, and if furthermore $a_n→ℓ$ and $c_n→ℓ$, then $b_n→ℓ$.

theorem sandwich (a b c : ℕ → ℝ)
(l : ℝ) (ha : is_limit a l) (hc : is_limit c l)
(hab : ∀ n, a n ≤ b n) (hbc : ∀ n, b n ≤ c n) : is_limit b l :=

Proof
We need to show that for all $ε>0$ there exists $N$ such that $n≥N$ implies $|b_n-ℓ|<ε$. So choose ε > 0.
  intros ε Hε,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n
⊢ is_limit b l

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |b n - l| < ε

we now need an $N$. As usual it is the max of two other N's, one coming from $(a_n)$ and one from $(c_n)$. Choose $N_a$ and $N_c$ such that $|aₙ - l| < ε$ for $n ≥ N_a$ and $|cₙ - l| < ε$ for $n ≥ N_c$.
  cases ha ε Hε with Na Ha,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |b n - l| < ε

  cases hc ε Hε with Nc Hc,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |b n - l| < ε

Now let $N$ be the max of $N_a$ and $N_c$; we claim that this works.
  let N := max Na Nc,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |b n - l| < ε

  use N,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc
⊢ ∀ (n : ℕ), n ≥ N → |b n - l| < ε

Note that $N ≥ N_a$ and $N ≥ N_c$,
  have HNa : Na ≤ N := by obvious_ineq,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc
⊢ ∀ (n : ℕ), n ≥ N → |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N
⊢ ∀ (n : ℕ), n ≥ N → |b n - l| < ε

  have HNc : Nc ≤ N := by obvious_ineq,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N
⊢ ∀ (n : ℕ), n ≥ N → |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N
⊢ ∀ (n : ℕ), n ≥ N → |b n - l| < ε

so for all n ≥ N,
  intros n Hn,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N
⊢ ∀ (n : ℕ), n ≥ N → |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N
⊢ |b n - l| < ε

we have $n≥ N_a$ and $n\geq N_c$, so $aₙ ≤ bₙ ≤ cₙ$, and $|aₙ - l|, |bₙ - l|$ are both less than $\epsilon$.
  have h1 : a n ≤ b n := hab n,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N
⊢ |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n
⊢ |b n - l| < ε

  have h2 : b n ≤ c n := hbc n,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n
⊢ |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n,
h2 : b n ≤ c n
⊢ |b n - l| < ε

  have h3 : |a n - l| < ε := Ha n (le_trans HNa Hn),

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n,
h2 : b n ≤ c n
⊢ |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n,
h2 : b n ≤ c n,
h3 : |a n - l| < ε
⊢ |b n - l| < ε

  have h4 : |c n - l| < ε := Hc n (le_trans HNc Hn),

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n,
h2 : b n ≤ c n,
h3 : |a n - l| < ε
⊢ |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n,
h2 : b n ≤ c n,
h3 : |a n - l| < ε,
h4 : |c n - l| < ε
⊢ |b n - l| < ε

The result now follows easily from these inequalities (as $l-ε<a_n≤b_n≤c_n<l+ε$).
  revert h3,revert h4,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n,
h2 : b n ≤ c n,
h3 : |a n - l| < ε,
h4 : |c n - l| < ε
⊢ |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n,
h2 : b n ≤ c n
⊢ |c n - l| < ε → |a n - l| < ε → |b n - l| < ε

  unfold abs,unfold max,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n,
h2 : b n ≤ c n
⊢ |c n - l| < ε → |a n - l| < ε → |b n - l| < ε

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n,
h2 : b n ≤ c n
⊢ ite (c n - l ≤ -(c n - l)) (-(c n - l)) (c n - l) < ε →
ite (a n - l ≤ -(a n - l)) (-(a n - l)) (a n - l) < ε → ite (b n - l ≤ -(b n - l)) (-(b n - l)) (b n - l) < ε

  split_ifs;intros;linarith,

a b c : ℕ → ℝ,
l : ℝ,
ha : is_limit a l,
hc : is_limit c l,
hab : ∀ (n : ℕ), a n ≤ b n,
hbc : ∀ (n : ℕ), b n ≤ c n,
ε : ℝ,
Hε : ε > 0,
Na : ℕ,
Ha : ∀ (n : ℕ), n ≥ Na → |a n - l| < ε,
Nc : ℕ,
Hc : ∀ (n : ℕ), n ≥ Nc → |c n - l| < ε,
N : ℕ := max Na Nc,
HNa : Na ≤ N,
HNc : Nc ≤ N,
n : ℕ,
Hn : n ≥ N,
h1 : a n ≤ b n,
h2 : b n ≤ c n
⊢ ite (c n - l ≤ -(c n - l)) (-(c n - l)) (c n - l) < ε →
ite (a n - l ≤ -(a n - l)) (-(a n - l)) (a n - l) < ε → ite (b n - l ≤ -(b n - l)) (-(b n - l)) (b n - l) < ε

no goals

QED.