𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
⊢ ∀ (s : Set E), s ∈ 𝓝 0 → (ε • x) ⁻¹' s ∈ l
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε : Tendsto ε l (𝓝 0)
⊢ Tendsto (ε • x) l (𝓝 0)
rw [tendsto_def] at *
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
⊢ (ε • x) ⁻¹' V ∈ l
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
⊢ ∀ (s : Set E), s ∈ 𝓝 0 → (ε • x) ⁻¹' s ∈ l
intro V hV
case intro.intro
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
⊢ (ε • x) ⁻¹' V ∈ l
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
⊢ (ε • x) ⁻¹' V ∈ l
rcases hS hV with ⟨r, r_pos, hrS⟩
case h
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
n : ι
hnS : x n ∈ S
hnr : n ∈ ε ⁻¹' Metric.ball 0 r⁻¹
⊢ n ∈ (ε • x) ⁻¹' V
case intro.intro
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
⊢ (ε • x) ⁻¹' V ∈ l
filter_upwards [hxS, hε _ (Metric.ball_mem_nhds 0 <| inv_pos.mpr r_pos)] with n hnS hnr
case pos
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε✝ : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
n : ι
hnS : x n ∈ S
hnr : n ∈ ε ⁻¹' Metric.ball 0 r⁻¹
hε : ε n = 0
⊢ n ∈ (ε • x) ⁻¹' V

case neg
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε✝ : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
n : ι
hnS : x n ∈ S
hnr : n ∈ ε ⁻¹' Metric.ball 0 r⁻¹
hε : ¬ε n = 0
⊢ n ∈ (ε • x) ⁻¹' V
case h
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
n : ι
hnS : x n ∈ S
hnr : n ∈ ε ⁻¹' Metric.ball 0 r⁻¹
⊢ n ∈ (ε • x) ⁻¹' V
by_cases hε : ε n = 0
no goals
case pos
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε✝ : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
n : ι
hnS : x n ∈ S
hnr : n ∈ ε ⁻¹' Metric.ball 0 r⁻¹
hε : ε n = 0
⊢ n ∈ (ε • x) ⁻¹' V
simp [hε, mem_of_mem_nhds hV]
case neg
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε✝ : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
n : ι
hnS : x n ∈ S
hnr : r < ‖(ε n)⁻¹‖
hε : ¬ε n = 0
⊢ n ∈ (ε • x) ⁻¹' V
case neg
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε✝ : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
n : ι
hnS : x n ∈ S
hnr : n ∈ ε ⁻¹' Metric.ball 0 r⁻¹
hε : ¬ε n = 0
⊢ n ∈ (ε • x) ⁻¹' V
rw [mem_preimage, mem_ball_zero_iff, lt_inv (norm_pos_iff.mpr hε) r_pos, ← norm_inv] at hnr
case neg
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε✝ : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
n : ι
hnS : x n ∈ S
hnr : r < ‖(ε n)⁻¹‖
hε : ¬ε n = 0
⊢ x n ∈ (ε n)⁻¹ • V
case neg
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε✝ : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
n : ι
hnS : x n ∈ S
hnr : r < ‖(ε n)⁻¹‖
hε : ¬ε n = 0
⊢ n ∈ (ε • x) ⁻¹' V
rw [mem_preimage, Pi.smul_apply', ← Set.mem_inv_smul_set_iff₀ hε]
no goals
case neg
𝕜 : Type u_3
𝕜' : Type ?u.156377
E : Type u_1
E' : Type ?u.156383
F : Type ?u.156386
ι : Type u_2
𝕝 : Type ?u.156392
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕝 E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε✝ : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ε ⁻¹' s ∈ l
V : Set E
hV : V ∈ 𝓝 0
r : ℝ
r_pos : 0 < r
hrS : ∀ (a : 𝕜), r ≤ ‖a‖ → S ⊆ a • V
n : ι
hnS : x n ∈ S
hnr : r < ‖(ε n)⁻¹‖
hε : ¬ε n = 0
⊢ x n ∈ (ε n)⁻¹ • V
exact hrS _ hnr.le hnS