[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
