Theorem: bolzano_weierstrass (LeanTeaching/TutoLib.lean)

State before:
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
⊢ ∃ c ∈ Icc a b, cluster_point u c
Tactic:
rcases (isCompact_Icc : IsCompact (Icc a b)).tendsto_subseq h with ⟨c, c_in, φ, hφ, lim⟩
State after:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : Tendsto ((fun n => u n) ∘ φ) atTop (nhds c)
⊢ ∃ c ∈ Icc a b, cluster_point u c

State before:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : Tendsto ((fun n => u n) ∘ φ) atTop (nhds c)
⊢ ∃ c ∈ Icc a b, cluster_point u c
Tactic:
refine ⟨c, c_in, φ, hφ, ?_⟩
State after:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : Tendsto ((fun n => u n) ∘ φ) atTop (nhds c)
⊢ seq_limit (u ∘ φ) c

State before:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : Tendsto ((fun n => u n) ∘ φ) atTop (nhds c)
⊢ seq_limit (u ∘ φ) c
Tactic:
simp_rw [Metric.tendsto_nhds, eventually_atTop, Real.dist_eq] at lim
State after:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
⊢ seq_limit (u ∘ φ) c

State before:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
⊢ seq_limit (u ∘ φ) c
Tactic:
intros ε ε_pos
State after:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε

State before:
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε
Tactic:
rcases lim ε ε_pos with ⟨N, hN⟩
State after:
case intro.intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε

State before:
case intro.intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε
Tactic:
use N
State after:
case h
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε

State before:
case h
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
⊢ ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε
Tactic:
intros n hn
State after:
case h
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - c| ≤ ε

State before:
case h
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - c| ≤ ε
Tactic:
exact le_of_lt (hN n hn)
State after:
no goals