[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
suffices ∀ᶠ r in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r
  by
  refine' ge_of_tendsto _ this
  exact (tendsto_const_nhds.div tendsto_id hR₁.ne').mono_left nhdsWithin_le_nhds
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this : ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
refine' ge_of_tendsto _ this
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this : ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
⊢ Tendsto (fun c => R₂ / c) (𝓝[Iio R₁] R₁) (𝓝 (R₂ / R₁))
[PROOFSTEP]
exact (tendsto_const_nhds.div tendsto_id hR₁.ne').mono_left nhdsWithin_le_nhds
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
[PROOFSTEP]
rw [mem_ball] at hz
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
⊢ ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
[PROOFSTEP]
filter_upwards [Ioo_mem_nhdsWithin_Iio ⟨hz, le_rfl⟩] with r hr
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
⊢ ‖dslope f c z‖ ≤ R₂ / r
[PROOFSTEP]
have hr₀ : 0 < r := dist_nonneg.trans_lt hr.1
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ ‖dslope f c z‖ ≤ R₂ / r
[PROOFSTEP]
replace hd : DiffContOnCl ℂ (dslope f c) (ball c r)
[GOAL]
case hd
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ DiffContOnCl ℂ (dslope f c) (ball c r)
[PROOFSTEP]
refine' DifferentiableOn.diffContOnCl _
[GOAL]
case hd
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ DifferentiableOn ℂ (dslope f c) (closure (ball c r))
[PROOFSTEP]
rw [closure_ball c hr₀.ne']
[GOAL]
case hd
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ DifferentiableOn ℂ (dslope f c) (closedBall c r)
[PROOFSTEP]
exact ((differentiableOn_dslope <| ball_mem_nhds _ hR₁).mpr hd).mono (closedBall_subset_ball hr.2)
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ ‖dslope f c z‖ ≤ R₂ / r
[PROOFSTEP]
refine' norm_le_of_forall_mem_frontier_norm_le bounded_ball hd _ _
[GOAL]
case h.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ ∀ (z : ℂ), z ∈ frontier (ball c r) → ‖dslope f c z‖ ≤ R₂ / r
[PROOFSTEP]
rw [frontier_ball c hr₀.ne']
[GOAL]
case h.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ ∀ (z : ℂ), z ∈ sphere c r → ‖dslope f c z‖ ≤ R₂ / r
[PROOFSTEP]
intro z hz
[GOAL]
case h.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
⊢ ‖dslope f c z‖ ≤ R₂ / r
[PROOFSTEP]
have hz' : z ≠ c := ne_of_mem_sphere hz hr₀.ne'
[GOAL]
case h.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / r
[PROOFSTEP]
rw [dslope_of_ne _ hz', slope_def_module, norm_smul, norm_inv, mem_sphere_iff_norm.1 hz, ← div_eq_inv_mul,
  div_le_div_right hr₀, ← dist_eq_norm]
[GOAL]
case h.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ dist (f z) (f c) ≤ R₂
[PROOFSTEP]
exact le_of_lt (h_maps (mem_ball.2 (by rw [mem_sphere.1 hz]; exact hr.2)))
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ dist z c < R₁
[PROOFSTEP]
rw [mem_sphere.1 hz]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ r < R₁
[PROOFSTEP]
exact hr.2
[GOAL]
case h.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ z ∈ closure (ball c r)
[PROOFSTEP]
rw [closure_ball c hr₀.ne', mem_closedBall]
[GOAL]
case h.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ dist z c ≤ r
[PROOFSTEP]
exact hr.1.le
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
have hR₂ : 0 < R₂ := nonempty_ball.1 ⟨f z, h_maps hz⟩
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
cases' eq_or_ne (dslope f c z) 0 with hc hc
[GOAL]
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z = 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
rw [hc, norm_zero]
[GOAL]
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z = 0
⊢ 0 ≤ R₂ / R₁
[PROOFSTEP]
exact div_nonneg hR₂.le hR₁.le
[GOAL]
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
rcases exists_dual_vector ℂ _ hc with ⟨g, hg, hgf⟩
[GOAL]
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
have hg' : ‖g‖₊ = 1 := NNReal.eq hg
[GOAL]
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
have hg₀ : ‖g‖₊ ≠ 0 := by simpa only [hg'] using one_ne_zero
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
⊢ ‖g‖₊ ≠ 0
[PROOFSTEP]
simpa only [hg'] using one_ne_zero
[GOAL]
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
[PROOFSTEP]
calc
  ‖dslope f c z‖ = ‖dslope (g ∘ f) c z‖ :=
    by
    rw [g.dslope_comp, hgf, IsROrC.norm_ofReal, abs_norm]
    exact fun _ => hd.differentiableAt (ball_mem_nhds _ hR₁)
  _ ≤ R₂ / R₁ :=
    by
    refine' schwarz_aux (g.differentiable.comp_differentiableOn hd) (MapsTo.comp _ h_maps) hz
    simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_ball hg₀ (f c) R₂
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope f c z‖ = ‖dslope (↑g ∘ f) c z‖
[PROOFSTEP]
rw [g.dslope_comp, hgf, IsROrC.norm_ofReal, abs_norm]
[GOAL]
case H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ c = z → DifferentiableAt ℂ f c
[PROOFSTEP]
exact fun _ => hd.differentiableAt (ball_mem_nhds _ hR₁)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope (↑g ∘ f) c z‖ ≤ R₂ / R₁
[PROOFSTEP]
refine' schwarz_aux (g.differentiable.comp_differentiableOn hd) (MapsTo.comp _ h_maps) hz
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : ↑g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ MapsTo (↑g) (ball (f c) R₂) (ball ((↑g ∘ f) c) R₂)
[PROOFSTEP]
simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_ball hg₀ (f c) R₂
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
⊢ EqOn f (fun z => f c + (z - c) • dslope f c z₀) (ball c R₁)
[PROOFSTEP]
set g := dslope f c
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
⊢ EqOn f (fun z => f c + (z - c) • g z₀) (ball c R₁)
[PROOFSTEP]
rintro z hz
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z✝ z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
⊢ f z = (fun z => f c + (z - c) • g z₀) z
[PROOFSTEP]
by_cases z = c
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z✝ z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
⊢ f z = (fun z => f c + (z - c) • g z₀) z
[PROOFSTEP]
by_cases z = c
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z✝ z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : z = c
⊢ f z = (fun z => f c + (z - c) • g z₀) z
[PROOFSTEP]
simp [h]
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z✝ z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
⊢ f z = (fun z => f c + (z - c) • g z₀) z
[PROOFSTEP]
have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z✝ z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
h_R₁ : 0 < R₁
⊢ f z = (fun z => f c + (z - c) • g z₀) z
[PROOFSTEP]
have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁ := fun z hz => norm_dslope_le_div_of_mapsTo_ball hd h_maps hz
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z✝ z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
h_R₁ : 0 < R₁
g_le_div : ∀ (z : ℂ), z ∈ ball c R₁ → ‖g z‖ ≤ R₂ / R₁
⊢ f z = (fun z => f c + (z - c) • g z₀) z
[PROOFSTEP]
have g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀ := isMaxOn_iff.mpr fun z hz => by simpa [h_eq] using g_le_div z hz
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z✝¹ z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z✝ : ℂ
hz✝ : z✝ ∈ ball c R₁
h : ¬z✝ = c
h_R₁ : 0 < R₁
g_le_div : ∀ (z : ℂ), z ∈ ball c R₁ → ‖g z‖ ≤ R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
⊢ (norm ∘ g) z ≤ (norm ∘ g) z₀
[PROOFSTEP]
simpa [h_eq] using g_le_div z hz
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z✝ z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
h_R₁ : 0 < R₁
g_le_div : ∀ (z : ℂ), z ∈ ball c R₁ → ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
⊢ f z = (fun z => f c + (z - c) • g z₀) z
[PROOFSTEP]
have g_diff : DifferentiableOn ℂ g (ball c R₁) :=
  (differentiableOn_dslope (isOpen_ball.mem_nhds (mem_ball_self h_R₁))).mpr hd
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z✝ z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
h_R₁ : 0 < R₁
g_le_div : ∀ (z : ℂ), z ∈ ball c R₁ → ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
⊢ f z = (fun z => f c + (z - c) • g z₀) z
[PROOFSTEP]
have : g z = g z₀ :=
  eqOn_of_isPreconnected_of_isMaxOn_norm (convex_ball c R₁).isPreconnected isOpen_ball g_diff h_z₀ g_max hz
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z✝ z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
h_R₁ : 0 < R₁
g_le_div : ∀ (z : ℂ), z ∈ ball c R₁ → ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
this : g z = g z₀
⊢ f z = (fun z => f c + (z - c) • g z₀) z
[PROOFSTEP]
simp [← this]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h₀ : 0 < R₁
⊢ ‖deriv f c‖ ≤ R₂ / R₁
[PROOFSTEP]
simpa only [dslope_same] using norm_dslope_le_div_of_mapsTo_ball hd h_maps (mem_ball_self h₀)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c
[PROOFSTEP]
rcases eq_or_ne z c with (rfl | hne)
[GOAL]
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball z R₁)
h_maps : MapsTo f (ball z R₁) (ball (f z) R₂)
hz : z ∈ ball z R₁
⊢ dist (f z) (f z) ≤ R₂ / R₁ * dist z z
[PROOFSTEP]
simp only [dist_self, mul_zero, le_rfl]
[GOAL]
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f : ℂ → E
c z z₀ : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c
[PROOFSTEP]
simpa only [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← div_eq_inv_mul, ← dist_eq_norm,
  div_le_iff (dist_pos.2 hne)] using norm_dslope_le_div_of_mapsTo_ball hd h_maps hz
[GOAL]
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
h₀ : 0 < R
⊢ MapsTo f (ball c R) (ball (f c) R)
[PROOFSTEP]
rwa [hc]
[GOAL]
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
⊢ dist (f z) c ≤ dist z c
[PROOFSTEP]
have := dist_le_div_mul_dist_of_mapsTo_ball hd (by rwa [hc]) hz
[GOAL]
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
⊢ MapsTo f (ball c R) (ball (f c) ?m.39633)
[PROOFSTEP]
rwa [hc]
[GOAL]
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
this : dist (f z) (f c) ≤ R / R * dist z c
⊢ dist (f z) c ≤ dist z c
[PROOFSTEP]
rwa [hc, div_self, one_mul] at this
[GOAL]
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (ball c R)
hc : f c = c
hz : z ∈ ball c R
this : dist (f z) c ≤ R / R * dist z c
⊢ R ≠ 0
[PROOFSTEP]
exact (nonempty_ball.1 ⟨z, hz⟩).ne'
[GOAL]
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (ball 0 R)
h₀ : f 0 = 0
hz : ↑abs z < R
⊢ ↑abs (f z) ≤ ↑abs z
[PROOFSTEP]
replace hz : z ∈ ball (0 : ℂ) R
[GOAL]
case hz
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (ball 0 R)
h₀ : f 0 = 0
hz : ↑abs z < R
⊢ z ∈ ball 0 R
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (ball 0 R)
h₀ : f 0 = 0
hz : z ∈ ball 0 R
⊢ ↑abs (f z) ≤ ↑abs z
[PROOFSTEP]
exact mem_ball_zero_iff.2 hz
[GOAL]
f : ℂ → ℂ
c z : ℂ
R R₁ R₂ : ℝ
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (ball 0 R)
h₀ : f 0 = 0
hz : z ∈ ball 0 R
⊢ ↑abs (f z) ≤ ↑abs z
[PROOFSTEP]
simpa only [dist_zero_right] using dist_le_dist_of_mapsTo_ball_self hd h_maps h₀ hz


[GOAL]
f : ℂ[X]
hf : 0 < degree f
⊢ ∃ z, IsRoot f z
[PROOFSTEP]
contrapose! hf
[GOAL]
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
⊢ degree f ≤ 0
[PROOFSTEP]
have : Metric.Bounded (Set.range (eval · f)⁻¹)
[GOAL]
case this
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
⊢ Metric.Bounded (Set.range (fun x => eval x f)⁻¹)
[PROOFSTEP]
obtain ⟨z₀, h₀⟩ := f.exists_forall_norm_le
[GOAL]
case this.intro
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
z₀ : ℂ
h₀ : ∀ (y : ℂ), ‖eval z₀ f‖ ≤ ‖eval y f‖
⊢ Metric.Bounded (Set.range (fun x => eval x f)⁻¹)
[PROOFSTEP]
simp only [Pi.inv_apply, bounded_iff_forall_norm_le, Set.forall_range_iff, norm_inv]
[GOAL]
case this.intro
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
z₀ : ℂ
h₀ : ∀ (y : ℂ), ‖eval z₀ f‖ ≤ ‖eval y f‖
⊢ ∃ C, ∀ (i : ℂ), ‖eval i f‖⁻¹ ≤ C
[PROOFSTEP]
exact ⟨‖eval z₀ f‖⁻¹, fun z => inv_le_inv_of_le (norm_pos_iff.2 <| hf z₀) (h₀ z)⟩
[GOAL]
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
this : Metric.Bounded (Set.range (fun x => eval x f)⁻¹)
⊢ degree f ≤ 0
[PROOFSTEP]
obtain ⟨c, hc⟩ := (f.differentiable.inv hf).exists_const_forall_eq_of_bounded this
[GOAL]
case intro
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
this : Metric.Bounded (Set.range (fun x => eval x f)⁻¹)
c : ℂ
hc : ∀ (z : ℂ), (eval z f)⁻¹ = c
⊢ degree f ≤ 0
[PROOFSTEP]
obtain rfl : f = C c⁻¹ := Polynomial.funext fun z => by rw [eval_C, ← hc z, inv_inv]
[GOAL]
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
this : Metric.Bounded (Set.range (fun x => eval x f)⁻¹)
c : ℂ
hc : ∀ (z : ℂ), (eval z f)⁻¹ = c
z : ℂ
⊢ eval z f = eval z (↑C c⁻¹)
[PROOFSTEP]
rw [eval_C, ← hc z, inv_inv]
[GOAL]
case intro
c : ℂ
hf : ∀ (z : ℂ), ¬IsRoot (↑C c⁻¹) z
this : Metric.Bounded (Set.range (fun x => eval x (↑C c⁻¹))⁻¹)
hc : ∀ (z : ℂ), (eval z (↑C c⁻¹))⁻¹ = c
⊢ degree (↑C c⁻¹) ≤ 0
[PROOFSTEP]
exact degree_C_le


[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
⊢ IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
[PROOFSTEP]
refine' ⟨fun hA i hi => hA (h.mem_of_mem hi), fun hA V hV => _⟩
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V A
[PROOFSTEP]
rcases h.mem_iff.mp hV with ⟨i, hi, hV⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV✝ : V ∈ 𝓝 0
i : ι
hi : q i
hV : s i ⊆ V
⊢ Absorbs 𝕜 V A
[PROOFSTEP]
exact (hA i hi).mono_left hV
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ IsVonNBounded 𝕜₂ (↑f '' s)
[PROOFSTEP]
let σ' := RingEquiv.ofBijective σ ⟨σ.injective, σ.surjective⟩
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
⊢ IsVonNBounded 𝕜₂ (↑f '' s)
[PROOFSTEP]
have σ_iso : Isometry σ := AddMonoidHomClass.isometry_of_norm σ fun x => RingHomIsometric.is_iso
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
⊢ IsVonNBounded 𝕜₂ (↑f '' s)
[PROOFSTEP]
have σ'_symm_iso : Isometry σ'.symm := σ_iso.right_inv σ'.right_inv
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
⊢ IsVonNBounded 𝕜₂ (↑f '' s)
[PROOFSTEP]
have f_tendsto_zero := f.continuous.tendsto 0
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 (↑f 0))
⊢ IsVonNBounded 𝕜₂ (↑f '' s)
[PROOFSTEP]
rw [map_zero] at f_tendsto_zero
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 0)
⊢ IsVonNBounded 𝕜₂ (↑f '' s)
[PROOFSTEP]
intro V hV
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 0)
V : Set F
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜₂ V (↑f '' s)
[PROOFSTEP]
rcases hs (f_tendsto_zero hV) with ⟨r, hrpos, hr⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 0)
V : Set F
hV : V ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜₁), r ≤ ‖a‖ → s ⊆ a • ↑f ⁻¹' V
⊢ Absorbs 𝕜₂ V (↑f '' s)
[PROOFSTEP]
refine' ⟨r, hrpos, fun a ha => _⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 0)
V : Set F
hV : V ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜₁), r ≤ ‖a‖ → s ⊆ a • ↑f ⁻¹' V
a : 𝕜₂
ha : r ≤ ‖a‖
⊢ ↑f '' s ⊆ a • V
[PROOFSTEP]
rw [← σ'.apply_symm_apply a]
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 0)
V : Set F
hV : V ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜₁), r ≤ ‖a‖ → s ⊆ a • ↑f ⁻¹' V
a : 𝕜₂
ha : r ≤ ‖a‖
⊢ ↑f '' s ⊆ ↑σ' (↑(RingEquiv.symm σ') a) • V
[PROOFSTEP]
have hanz : a ≠ 0 := norm_pos_iff.mp (hrpos.trans_le ha)
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 0)
V : Set F
hV : V ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜₁), r ≤ ‖a‖ → s ⊆ a • ↑f ⁻¹' V
a : 𝕜₂
ha : r ≤ ‖a‖
hanz : a ≠ 0
⊢ ↑f '' s ⊆ ↑σ' (↑(RingEquiv.symm σ') a) • V
[PROOFSTEP]
have : σ'.symm a ≠ 0 := (map_ne_zero σ'.symm.toRingHom).mpr hanz
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 0)
V : Set F
hV : V ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜₁), r ≤ ‖a‖ → s ⊆ a • ↑f ⁻¹' V
a : 𝕜₂
ha : r ≤ ‖a‖
hanz : a ≠ 0
this : ↑(RingEquiv.symm σ') a ≠ 0
⊢ ↑f '' s ⊆ ↑σ' (↑(RingEquiv.symm σ') a) • V
[PROOFSTEP]
change _ ⊆ σ _ • _
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 0)
V : Set F
hV : V ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜₁), r ≤ ‖a‖ → s ⊆ a • ↑f ⁻¹' V
a : 𝕜₂
ha : r ≤ ‖a‖
hanz : a ≠ 0
this : ↑(RingEquiv.symm σ') a ≠ 0
⊢ ↑f '' s ⊆ ↑σ (↑(RingEquiv.symm σ') a) • V
[PROOFSTEP]
rw [Set.image_subset_iff, preimage_smul_setₛₗ _ _ _ f this.isUnit]
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 0)
V : Set F
hV : V ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜₁), r ≤ ‖a‖ → s ⊆ a • ↑f ⁻¹' V
a : 𝕜₂
ha : r ≤ ‖a‖
hanz : a ≠ 0
this : ↑(RingEquiv.symm σ') a ≠ 0
⊢ s ⊆ ↑(RingEquiv.symm σ') a • ↑f ⁻¹' V
[PROOFSTEP]
refine' hr (σ'.symm a) _
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕜₁ : Type u_7
𝕜₂ : Type u_8
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
σ' : 𝕜₁ ≃+* 𝕜₂ := RingEquiv.ofBijective σ (_ : Function.Injective ↑σ ∧ Function.Surjective ↑σ)
σ_iso : Isometry ↑σ
σ'_symm_iso : Isometry ↑(RingEquiv.symm σ')
f_tendsto_zero : Tendsto (↑f) (𝓝 0) (𝓝 0)
V : Set F
hV : V ∈ 𝓝 0
r : ℝ
hrpos : 0 < r
hr : ∀ (a : 𝕜₁), r ≤ ‖a‖ → s ⊆ a • ↑f ⁻¹' V
a : 𝕜₂
ha : r ≤ ‖a‖
hanz : a ≠ 0
this : ↑(RingEquiv.symm σ') a ≠ 0
⊢ r ≤ ‖↑(RingEquiv.symm σ') a‖
[PROOFSTEP]
rwa [σ'_symm_iso.norm_map_of_map_zero (map_zero _)]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
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)
[PROOFSTEP]
rw [tendsto_def] at *
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
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
[PROOFSTEP]
intro V hV
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
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
[PROOFSTEP]
rcases hS hV with ⟨r, r_pos, hrS⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
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
[PROOFSTEP]
filter_upwards [hxS, hε _ (Metric.ball_mem_nhds 0 <| inv_pos.mpr r_pos)] with n hnS hnr
[GOAL]
case h
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
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
[PROOFSTEP]
by_cases hε : ε n = 0
[GOAL]
case pos
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
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
[PROOFSTEP]
simp [hε, mem_of_mem_nhds hV]
[GOAL]
case neg
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
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
[PROOFSTEP]
rw [mem_preimage, mem_ball_zero_iff, lt_inv (norm_pos_iff.mpr hε) r_pos, ← norm_inv] at hnr
[GOAL]
case neg
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
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
[PROOFSTEP]
rw [mem_preimage, Pi.smul_apply', ← Set.mem_inv_smul_set_iff₀ hε]
[GOAL]
case neg
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
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
[PROOFSTEP]
exact hrS _ hnr.le hnS
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
⊢ IsVonNBounded 𝕝 S
[PROOFSTEP]
rw [(nhds_basis_balanced 𝕝 E).isVonNBounded_basis_iff]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
⊢ ∀ (i : Set E), i ∈ 𝓝 0 ∧ Balanced 𝕝 i → Absorbs 𝕝 (id i) S
[PROOFSTEP]
by_contra' H'
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
H' : ∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕝 i) ∧ ¬Absorbs 𝕝 (id i) S
⊢ False
[PROOFSTEP]
rcases H' with ⟨V, ⟨hV, hVb⟩, hVS⟩
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕝 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
⊢ False
[PROOFSTEP]
have : ∀ᶠ n in l, ∃ x : S, ε n • (x : E) ∉ V :=
  by
  filter_upwards [hε] with n hn
  rw [Absorbs] at hVS
  push_neg at hVS
  rcases hVS _ (norm_pos_iff.mpr <| inv_ne_zero hn) with ⟨a, haε, haS⟩
  rcases Set.not_subset.mp haS with ⟨x, hxS, hx⟩
  refine' ⟨⟨x, hxS⟩, fun hnx => _⟩
  rw [← Set.mem_inv_smul_set_iff₀ hn] at hnx
  exact hx (hVb.smul_mono haε hnx)
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕝 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
⊢ ∀ᶠ (n : ι) in l, ∃ x, ¬ε n • ↑x ∈ V
[PROOFSTEP]
filter_upwards [hε] with n hn
[GOAL]
case h
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕝 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
n : ι
hn : ε n ≠ 0
⊢ ∃ x, ¬ε n • ↑x ∈ V
[PROOFSTEP]
rw [Absorbs] at hVS
[GOAL]
case h
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬∃ r, 0 < r ∧ ∀ (a : 𝕝), r ≤ ‖a‖ → S ⊆ a • id V
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
n : ι
hn : ε n ≠ 0
⊢ ∃ x, ¬ε n • ↑x ∈ V
[PROOFSTEP]
push_neg at hVS
[GOAL]
case h
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), 0 < r → ∃ a, r ≤ ‖a‖ ∧ ¬S ⊆ a • id V
⊢ ∃ x, ¬ε n • ↑x ∈ V
[PROOFSTEP]
rcases hVS _ (norm_pos_iff.mpr <| inv_ne_zero hn) with ⟨a, haε, haS⟩
[GOAL]
case h.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), 0 < r → ∃ a, r ≤ ‖a‖ ∧ ¬S ⊆ a • id V
a : 𝕝
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
⊢ ∃ x, ¬ε n • ↑x ∈ V
[PROOFSTEP]
rcases Set.not_subset.mp haS with ⟨x, hxS, hx⟩
[GOAL]
case h.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), 0 < r → ∃ a, r ≤ ‖a‖ ∧ ¬S ⊆ a • id V
a : 𝕝
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
x : E
hxS : x ∈ S
hx : ¬x ∈ a • id V
⊢ ∃ x, ¬ε n • ↑x ∈ V
[PROOFSTEP]
refine' ⟨⟨x, hxS⟩, fun hnx => _⟩
[GOAL]
case h.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), 0 < r → ∃ a, r ≤ ‖a‖ ∧ ¬S ⊆ a • id V
a : 𝕝
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
x : E
hxS : x ∈ S
hx : ¬x ∈ a • id V
hnx : ε n • ↑{ val := x, property := hxS } ∈ V
⊢ False
[PROOFSTEP]
rw [← Set.mem_inv_smul_set_iff₀ hn] at hnx
[GOAL]
case h.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), 0 < r → ∃ a, r ≤ ‖a‖ ∧ ¬S ⊆ a • id V
a : 𝕝
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
x : E
hxS : x ∈ S
hx : ¬x ∈ a • id V
hnx : ↑{ val := x, property := hxS } ∈ (ε n)⁻¹ • V
⊢ False
[PROOFSTEP]
exact hx (hVb.smul_mono haε hnx)
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕝 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
this : ∀ᶠ (n : ι) in l, ∃ x, ¬ε n • ↑x ∈ V
⊢ False
[PROOFSTEP]
rcases this.choice with ⟨x, hx⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕝 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
this : ∀ᶠ (n : ι) in l, ∃ x, ¬ε n • ↑x ∈ V
x : ι → ↑S
hx : ∀ᶠ (x_1 : ι) in l, ¬ε x_1 • ↑(x x_1) ∈ V
⊢ False
[PROOFSTEP]
refine' Filter.frequently_false l (Filter.Eventually.frequently _)
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕝 (id V) S
hV : V ∈ 𝓝 0
hVb : Balanced 𝕝 V
this : ∀ᶠ (n : ι) in l, ∃ x, ¬ε n • ↑x ∈ V
x : ι → ↑S
hx : ∀ᶠ (x_1 : ι) in l, ¬ε x_1 • ↑(x x_1) ∈ V
⊢ ∀ᶠ (x : ι) in l, False
[PROOFSTEP]
filter_upwards [hx, (H (_ ∘ x) fun n => (x n).2).eventually (eventually_mem_set.mpr hV)] using fun n => id
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
𝕝 : Type u_7
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : Tendsto ε l (𝓝[{0}ᶜ] 0)
S : Set E
⊢ ∀ᶠ (n : ι) in l, ε n ≠ 0
[PROOFSTEP]
exact hε self_mem_nhdsWithin
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
⊢ Bornology.IsVonNBounded 𝕜 s
[PROOFSTEP]
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
⊢ Bornology.IsVonNBounded 𝕜 s
[PROOFSTEP]
intro U hU
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 U s
[PROOFSTEP]
have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 ((0 : E) + (0 : E))) := tendsto_add
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 (0 + 0))
⊢ Absorbs 𝕜 U s
[PROOFSTEP]
rw [add_zero] at h
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
⊢ Absorbs 𝕜 U s
[PROOFSTEP]
have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 0 ×ˢ 𝓝 0) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    id i.fst ×ˢ id i.snd
⊢ Absorbs 𝕜 U s
[PROOFSTEP]
simp_rw [← nhds_prod_eq, id.def] at h'
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
⊢ Absorbs 𝕜 U s
[PROOFSTEP]
rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : TotallyBounded s
hs : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
⊢ Absorbs 𝕜 U s
[PROOFSTEP]
rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ Absorbs 𝕜 U s
[PROOFSTEP]
refine' Absorbs.mono_right _ hs
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ Absorbs 𝕜 U (⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd)
[PROOFSTEP]
rw [ht.absorbs_iUnion]
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ ∀ (i : E), i ∈ t → Absorbs 𝕜 U (i +ᵥ x.snd)
[PROOFSTEP]
have hx_fstsnd : x.fst + x.snd ⊆ U := by
  intro z hz
  rcases Set.mem_add.mp hz with ⟨z1, z2, hz1, hz2, hz⟩
  have hz' : (z1, z2) ∈ x.fst ×ˢ x.snd := ⟨hz1, hz2⟩
  simpa only [hz] using h'' hz'
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
⊢ x.fst + x.snd ⊆ U
[PROOFSTEP]
intro z hz
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
z : E
hz : z ∈ x.fst + x.snd
⊢ z ∈ U
[PROOFSTEP]
rcases Set.mem_add.mp hz with ⟨z1, z2, hz1, hz2, hz⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
z : E
hz✝ : z ∈ x.fst + x.snd
z1 z2 : E
hz1 : z1 ∈ x.fst
hz2 : z2 ∈ x.snd
hz : z1 + z2 = z
⊢ z ∈ U
[PROOFSTEP]
have hz' : (z1, z2) ∈ x.fst ×ˢ x.snd := ⟨hz1, hz2⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
z : E
hz✝ : z ∈ x.fst + x.snd
z1 z2 : E
hz1 : z1 ∈ x.fst
hz2 : z2 ∈ x.snd
hz : z1 + z2 = z
hz' : (z1, z2) ∈ x.fst ×ˢ x.snd
⊢ z ∈ U
[PROOFSTEP]
simpa only [hz] using h'' hz'
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
hx_fstsnd : x.fst + x.snd ⊆ U
⊢ ∀ (i : E), i ∈ t → Absorbs 𝕜 U (i +ᵥ x.snd)
[PROOFSTEP]
refine' fun y _ => Absorbs.mono_left _ hx_fstsnd
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
hx_fstsnd : x.fst + x.snd ⊆ U
y : E
x✝ : y ∈ t
⊢ Absorbs 𝕜 (x.fst + x.snd) (y +ᵥ x.snd)
[PROOFSTEP]
rw [← Set.singleton_vadd, vadd_eq_add]
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝¹ : TotallyBounded s
hs✝ : ∀ (U : Set E), U ∈ 𝓝 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ U
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst + x.snd) (𝓝 (0, 0)) (𝓝 0)
h' :
  HasBasis (𝓝 (0, 0)) (fun i => (i.fst ∈ 𝓝 0 ∧ Balanced 𝕜 i.fst) ∧ i.snd ∈ 𝓝 0 ∧ Balanced 𝕜 i.snd) fun i =>
    i.fst ×ˢ i.snd
x : Set E × Set E
hx : (x.fst ∈ 𝓝 0 ∧ Balanced 𝕜 x.fst) ∧ x.snd ∈ 𝓝 0 ∧ Balanced 𝕜 x.snd
h'' : MapsTo (fun x => x.fst + x.snd) (x.fst ×ˢ x.snd) U
t : Set E
ht : Set.Finite t
hs : s ⊆ ⋃ (y : E) (_ : y ∈ t), y +ᵥ x.snd
hx_fstsnd : x.fst + x.snd ⊆ U
y : E
x✝ : y ∈ t
⊢ Absorbs 𝕜 (x.fst + x.snd) ({y} + x.snd)
[PROOFSTEP]
exact (absorbent_nhds_zero hx.1.1).absorbs.add hx.2.2.absorbs_self
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Bornology.IsVonNBounded 𝕜 (Metric.ball 0 r)
[PROOFSTEP]
rw [Metric.nhds_basis_ball.isVonNBounded_basis_iff, ← ball_normSeminorm 𝕜 E]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 i) (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
[PROOFSTEP]
exact fun ε hε => (normSeminorm 𝕜 E).ball_zero_absorbs_ball_zero hε
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ r < r + 1
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
[PROOFSTEP]
rw [← Metric.bounded_iff_isBounded, Metric.bounded_iff_subset_ball (0 : E)]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, s ⊆ Metric.closedBall 0 r
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s → ∃ r, s ⊆ Metric.closedBall 0 r
[PROOFSTEP]
intro h
[GOAL]
case mp
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
[PROOFSTEP]
rcases h (Metric.ball_mem_nhds 0 zero_lt_one) with ⟨ρ, hρ, hρball⟩
[GOAL]
case mp.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
hρball : ∀ (a : 𝕜), ρ ≤ ‖a‖ → s ⊆ a • Metric.ball 0 1
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
[PROOFSTEP]
rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩
[GOAL]
case mp.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
hρball : ∀ (a : 𝕜), ρ ≤ ‖a‖ → s ⊆ a • Metric.ball 0 1
a : 𝕜
ha : ρ < ‖a‖
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
[PROOFSTEP]
specialize hρball a ha.le
[GOAL]
case mp.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ a • Metric.ball 0 1
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
[PROOFSTEP]
rw [← ball_normSeminorm 𝕜 E, Seminorm.smul_ball_zero (norm_pos_iff.1 <| hρ.trans ha), ball_normSeminorm, mul_one] at
  hρball
[GOAL]
case mp.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : 0 < ρ
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ Metric.ball 0 ‖a‖
⊢ ∃ r, s ⊆ Metric.closedBall 0 r
[PROOFSTEP]
exact ⟨‖a‖, hρball.trans Metric.ball_subset_closedBall⟩
[GOAL]
case mpr
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ r, s ⊆ Metric.closedBall 0 r) → Bornology.IsVonNBounded 𝕜 s
[PROOFSTEP]
exact fun ⟨C, hC⟩ => (isVonNBounded_closedBall 𝕜 E C).subset hC
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, ∀ (x : E), x ∈ s → ‖x‖ ≤ r
[PROOFSTEP]
rw [NormedSpace.isVonNBounded_iff, ← Metric.bounded_iff_isBounded, bounded_iff_forall_norm_le]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E' → E
s : Set E'
⊢ Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r, ∀ (x : E'), x ∈ s → ‖f x‖ ≤ r
[PROOFSTEP]
simp_rw [isVonNBounded_iff', Set.ball_image_iff]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology
[PROOFSTEP]
rw [Bornology.ext_iff_isBounded]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
[PROOFSTEP]
intro s
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s
[PROOFSTEP]
rw [Bornology.isBounded_iff_isVonNBounded]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
[PROOFSTEP]
exact isVonNBounded_iff 𝕜 E s
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.ball 0 1
[PROOFSTEP]
rw [← isVonNBounded_iff 𝕜]
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ a, s ⊆ a • Metric.ball 0 1
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s → ∃ a, s ⊆ a • Metric.ball 0 1
[PROOFSTEP]
intro h
[GOAL]
case mp
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ a, s ⊆ a • Metric.ball 0 1
[PROOFSTEP]
rcases h (Metric.ball_mem_nhds 0 zero_lt_one) with ⟨ρ, _, hρball⟩
[GOAL]
case mp.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
left✝ : 0 < ρ
hρball : ∀ (a : 𝕜), ρ ≤ ‖a‖ → s ⊆ a • Metric.ball 0 1
⊢ ∃ a, s ⊆ a • Metric.ball 0 1
[PROOFSTEP]
rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩
[GOAL]
case mp.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
left✝ : 0 < ρ
hρball : ∀ (a : 𝕜), ρ ≤ ‖a‖ → s ⊆ a • Metric.ball 0 1
a : 𝕜
ha : ρ < ‖a‖
⊢ ∃ a, s ⊆ a • Metric.ball 0 1
[PROOFSTEP]
exact ⟨a, hρball a ha.le⟩
[GOAL]
case mpr
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.ball 0 1) → Bornology.IsVonNBounded 𝕜 s
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case mpr.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ a • Metric.ball 0 1
⊢ Bornology.IsVonNBounded 𝕜 s
[PROOFSTEP]
exact ((isVonNBounded_ball 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.closedBall 0 1
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s → ∃ a, s ⊆ a • Metric.closedBall 0 1
[PROOFSTEP]
rw [isBounded_iff_subset_smul_ball 𝕜]
[GOAL]
case mp
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.ball 0 1) → ∃ a, s ⊆ a • Metric.closedBall 0 1
[PROOFSTEP]
exact Exists.imp fun a ha => ha.trans <| Set.smul_set_mono <| Metric.ball_subset_closedBall
[GOAL]
case mpr
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsBounded s
[PROOFSTEP]
rw [← isVonNBounded_iff 𝕜]
[GOAL]
case mpr
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsVonNBounded 𝕜 s
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case mpr.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
ι : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ a • Metric.closedBall 0 1
⊢ Bornology.IsVonNBounded 𝕜 s
[PROOFSTEP]
exact ((isVonNBounded_closedBall 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha