β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
⊢ ↑f ⁻¹' s ∈ atTop
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
⊢ ∀ (s : Set β), IsOpen s → lim f ∈ s → ↑f ⁻¹' s ∈ atTop
intro s os lfs
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
⊢ ↑f ⁻¹' s ∈ atTop
suffices ∃ a : ℕ, ∀ b : ℕ, b ≥ a → f b ∈ s by simpa using this
case intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
rcases Metric.isOpen_iff.1 os _ lfs with ⟨ε, ⟨hε, hεs⟩⟩
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
case intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
cases' Setoid.symm (CauSeq.equiv_lim f) _ hε with N hN
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
⊢ ∀ (b : ℕ), b ≥ N → ↑f b ∈ s
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
exists N
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ↑f b ∈ s
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
⊢ ∀ (b : ℕ), b ≥ N → ↑f b ∈ s
intro b hb
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ↑f b ∈ Metric.ball (lim f) ε
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ↑f b ∈ s
apply hεs
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ dist (↑f b) (lim f) < ε
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ↑f b ∈ Metric.ball (lim f) ε
dsimp [Metric.ball]
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ‖lim f - ↑f b‖ < ε
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ dist (↑f b) (lim f) < ε
rw [dist_comm, dist_eq_norm]
no goals
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ‖lim f - ↑f b‖ < ε
solve_by_elim
no goals
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
this : ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
⊢ ↑f ⁻¹' s ∈ atTop
simpa using this