𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
⊢ False
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
⊢ ContinuousAt (↑f) 0
by_contra h
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => _root_.id (b i)
⊢ False
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
⊢ False
rcases(nhds_basis_balanced 𝕜 E).exists_antitone_subbasis with ⟨b, bE1, bE⟩
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
⊢ False
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => _root_.id (b i)
⊢ False
simp only [id.def] at bE
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
h : ¬∀ (ib : Set F), ib ∈ 𝓝 0 ∧ Balanced 𝕜' ib → ∃ ia, ia ≠ 0 ∧ ∀ (x : E), x ∈ (↑ia)⁻¹ • b ia → ↑f x ∈ _root_.id ib
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
⊢ False
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
⊢ False
rw [ContinuousAt, map_zero, bE'.tendsto_iff (nhds_basis_balanced 𝕜' F)] at h
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
h : ∃ ib, (ib ∈ 𝓝 0 ∧ Balanced 𝕜' ib) ∧ ∀ (ia : ℕ), ia ≠ 0 → ∃ x, x ∈ (↑ia)⁻¹ • b ia ∧ ¬↑f x ∈ _root_.id ib
⊢ False
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
h : ¬∀ (ib : Set F), ib ∈ 𝓝 0 ∧ Balanced 𝕜' ib → ∃ ia, ia ≠ 0 ∧ ∀ (x : E), x ∈ (↑ia)⁻¹ • b ia → ↑f x ∈ _root_.id ib
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
⊢ False
push_neg at h
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
h : ∀ (ia : ℕ), ia ≠ 0 → ∃ x, x ∈ (↑ia)⁻¹ • b ia ∧ ¬↑f x ∈ _root_.id V
hV : V ∈ 𝓝 0
⊢ False
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
h : ∃ ib, (ib ∈ 𝓝 0 ∧ Balanced 𝕜' ib) ∧ ∀ (ia : ℕ), ia ≠ 0 → ∃ x, x ∈ (↑ia)⁻¹ • b ia ∧ ¬↑f x ∈ _root_.id ib
⊢ False
rcases h with ⟨V, ⟨hV, -⟩, h⟩
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
h : ∀ (ia : ℕ), ia ≠ 0 → ∃ x, x ∈ (↑ia)⁻¹ • b ia ∧ ¬↑f x ∈ V
hV : V ∈ 𝓝 0
⊢ False
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
h : ∀ (ia : ℕ), ia ≠ 0 → ∃ x, x ∈ (↑ia)⁻¹ • b ia ∧ ¬↑f x ∈ _root_.id V
hV : V ∈ 𝓝 0
⊢ False
simp only [id.def, forall_true_left] at h
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
⊢ False
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
h : ∀ (ia : ℕ), ia ≠ 0 → ∃ x, x ∈ (↑ia)⁻¹ • b ia ∧ ¬↑f x ∈ V
hV : V ∈ 𝓝 0
⊢ False
choose! u hu hu' using h
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
⊢ False
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
⊢ False
have h_bounded : IsVonNBounded 𝕜 (Set.range fun n : ℕ => (n : 𝕜) • u n) :=
  h_tendsto.cauchySeq.totallyBounded_range.isVonNBounded 𝕜
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
⊢ False
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
⊢ False
rcases hf _ h_bounded hV with ⟨r, hr, h'⟩
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
⊢ False
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
⊢ False
cases' exists_nat_gt r with n hn
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
⊢ False
have h1 : r ≤ ‖(n : 𝕜')‖ := by
  rw [IsROrC.norm_natCast]
  exact hn.le
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : 0 < ‖↑n‖
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
⊢ False
have hn' : 0 < ‖(n : 𝕜')‖ := lt_of_lt_of_le hr h1
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : 0 < ‖↑n‖
⊢ False
rw [norm_pos_iff, Ne.def, Nat.cast_eq_zero] at hn'
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h'' : ↑f (u n) ∈ V
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
⊢ False
have h'' : f (u n) ∈ V := by
  simp only [Set.image_subset_iff] at h'
  specialize h' (n : 𝕜') h1 (Set.mem_range_self n)
  simp only [Set.mem_preimage, LinearMap.map_smulₛₗ, map_natCast] at h'
  rcases h' with ⟨y, hy, h'⟩
  apply_fun fun y : F => (n : 𝕜')⁻¹ • y  at h'
  simp only [hn', inv_smul_smul₀, Ne.def, Nat.cast_eq_zero, not_false_iff] at h'
  rwa [← h']
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h'' : ↑f (u n) ∈ V
⊢ False
exact hu' n hn' h''
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
⊢ ∀ (i : ℕ), True → ∃ i', i' ≠ 0 ∧ (↑i')⁻¹ • b i' ⊆ b i

case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
⊢ ∀ (i' : ℕ), i' ≠ 0 → ∃ i, True ∧ b i ⊆ (↑i')⁻¹ • b i'
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
⊢ HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
refine' bE.1.to_hasBasis _ _
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
⊢ ∀ (i' : ℕ), i' ≠ 0 → ∃ i, True ∧ b i ⊆ (↑i')⁻¹ • b i'
intro n hn
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ContinuousAt (fun x => ↑n • x) 0
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
have hcont : ContinuousAt (fun x : E => (n : 𝕜) • x) 0 :=
  (continuous_const_smul (n : 𝕜)).continuousAt
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : Tendsto (fun x => ↑n • x) (𝓝 0) (𝓝 0)
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ContinuousAt (fun x => ↑n • x) 0
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
simp only [ContinuousAt, map_zero, smul_zero] at hcont
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ (t : Set E), t ∈ 𝓝 0 → ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : Tendsto (fun x => ↑n • x) (𝓝 0) (𝓝 0)
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
rw [bE.1.tendsto_left_iff] at hcont
case refine'_2.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ (t : Set E), t ∈ 𝓝 0 → ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
i : ℕ
left✝ : True
hi : Set.MapsTo (fun x => ↑n • x) (b i) (b n)
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
case refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ (t : Set E), t ∈ 𝓝 0 → ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
rcases hcont (b n) (bE1 n).1 with ⟨i, _, hi⟩
case refine'_2.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ (t : Set E), t ∈ 𝓝 0 → ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
i : ℕ
left✝ : True
hi : Set.MapsTo (fun x => ↑n • x) (b i) (b n)
x : E
hx : x ∈ b i
⊢ (fun x => (↑n)⁻¹ • x) (↑n • x) = x
case refine'_2.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ (t : Set E), t ∈ 𝓝 0 → ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
i : ℕ
left✝ : True
hi : Set.MapsTo (fun x => ↑n • x) (b i) (b n)
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n
refine' ⟨i, trivial, fun x hx => ⟨(n : 𝕜) • x, hi hx, _⟩⟩
no goals
case refine'_2.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ∀ (t : Set E), t ∈ 𝓝 0 → ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
i : ℕ
left✝ : True
hi : Set.MapsTo (fun x => ↑n • x) (b i) (b n)
x : E
hx : x ∈ b i
⊢ (fun x => (↑n)⁻¹ • x) (↑n • x) = x
simp [← mul_smul, hn]
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ ∃ i', i' ≠ 0 ∧ (↑i')⁻¹ • b i' ⊆ b n
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
⊢ ∀ (i : ℕ), True → ∃ i', i' ≠ 0 ∧ (↑i')⁻¹ • b i' ⊆ b i
intro n _
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ n + 1 ≠ 0 ∧ (↑(n + 1))⁻¹ • b (n + 1) ⊆ b n
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ ∃ i', i' ≠ 0 ∧ (↑i')⁻¹ • b i' ⊆ b n
use n + 1
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ (↑n + 1)⁻¹ • b (n + 1) ⊆ b n
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ n + 1 ≠ 0 ∧ (↑(n + 1))⁻¹ • b (n + 1) ⊆ b n
simp only [Ne.def, Nat.succ_ne_zero, not_false_iff, Nat.cast_add, Nat.cast_one, true_and_iff]
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
⊢ (↑n + 1)⁻¹ • b (n + 1) ⊆ b n
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ (↑n + 1)⁻¹ • b (n + 1) ⊆ b n
have h : b (n + 1) ⊆ b n := bE.2 (by simp)
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
⊢ (↑n + 1)⁻¹ • b (n + 1) ⊆ b (n + 1)
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
⊢ (↑n + 1)⁻¹ • b (n + 1) ⊆ b n
refine' _root_.trans _ h
case refine'_1.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
⊢ y ∈ b (n + 1)
case refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
⊢ (↑n + 1)⁻¹ • b (n + 1) ⊆ b (n + 1)
rintro y ⟨x, hx, hy⟩
case refine'_1.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
⊢ (fun x => (↑n + 1)⁻¹ • x) x ∈ b (n + 1)
case refine'_1.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
⊢ y ∈ b (n + 1)
rw [← hy]
case refine'_1.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
⊢ ‖(↑n + 1)⁻¹‖ ≤ 1
case refine'_1.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
⊢ (fun x => (↑n + 1)⁻¹ • x) x ∈ b (n + 1)
refine' (bE1 (n + 1)).2.smul_mem _ hx
case refine'_1.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
h' : 0 < ↑n + 1
⊢ ‖(↑n + 1)⁻¹‖ ≤ 1
case refine'_1.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
⊢ ‖(↑n + 1)⁻¹‖ ≤ 1
have h' : 0 < (n : ℝ) + 1 := n.cast_add_one_pos
case refine'_1.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
h' : 0 < ↑n + 1
⊢ 1⁻¹ ≤ ↑n + 1
case refine'_1.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
h' : 0 < ↑n + 1
⊢ ‖(↑n + 1)⁻¹‖ ≤ 1
rw [norm_inv, ← Nat.cast_one, ← Nat.cast_add, IsROrC.norm_natCast, Nat.cast_add, Nat.cast_one,
  inv_le h' zero_lt_one]
no goals
case refine'_1.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h✝ : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
h : b (n + 1) ⊆ b n
y x : E
hx : x ∈ b (n + 1)
hy : (fun x => (↑n + 1)⁻¹ • x) x = y
h' : 0 < ↑n + 1
⊢ 1⁻¹ ≤ ↑n + 1
simp
no goals
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
h : ¬ContinuousAt (↑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
n : ℕ
a✝ : True
⊢ n ≤ n + 1
simp
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
⊢ ∀ (i : ℕ), ↑i • u i ∈ b i
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
⊢ Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
apply bE.tendsto
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
⊢ ↑n • u n ∈ b n
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
⊢ ∀ (i : ℕ), ↑i • u i ∈ b i
intro n
case pos
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : n = 0
⊢ ↑n • u n ∈ b n

case neg
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
⊢ ↑n • u n ∈ b n
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
⊢ ↑n • u n ∈ b n
by_cases h : n = 0
case neg.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
y : E
hy : y ∈ b n
hu1 : (fun x => (↑n)⁻¹ • x) y = u n
⊢ ↑n • u n ∈ b n
case neg
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
⊢ ↑n • u n ∈ b n
rcases hu n h with ⟨y, hy, hu1⟩
case h.e'_4
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
y : E
hy : y ∈ b n
hu1 : (fun x => (↑n)⁻¹ • x) y = u n
⊢ ↑n • u n = y
case neg.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
y : E
hy : y ∈ b n
hu1 : (fun x => (↑n)⁻¹ • x) y = u n
⊢ ↑n • u n ∈ b n
convert hy
case h.e'_4
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
y : E
hy : y ∈ b n
hu1 : (fun x => (↑n)⁻¹ • x) y = u n
⊢ (↑n * (↑n)⁻¹) • y = y
case h.e'_4
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
y : E
hy : y ∈ b n
hu1 : (fun x => (↑n)⁻¹ • x) y = u n
⊢ ↑n • u n = y
rw [← hu1, ← mul_smul]
no goals
case h.e'_4
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : ¬n = 0
y : E
hy : y ∈ b n
hu1 : (fun x => (↑n)⁻¹ • x) y = u n
⊢ (↑n * (↑n)⁻¹) • y = y
simp only [h, mul_inv_cancel, Ne.def, Nat.cast_eq_zero, not_false_iff, one_smul]
case pos
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : n = 0
⊢ 0 ∈ b 0
case pos
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : n = 0
⊢ ↑n • u n ∈ b n
rw [h, Nat.cast_zero, zero_smul]
no goals
case pos
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : n = 0
⊢ 0 ∈ b 0
refine' mem_of_mem_nhds (bE.1.mem_of_mem <| by triv)
no goals
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
n : ℕ
h : n = 0
⊢ True
triv
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
⊢ r ≤ ↑n
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
⊢ r ≤ ‖↑n‖
rw [IsROrC.norm_natCast]
no goals
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
⊢ r ≤ ↑n
exact hn.le
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (Set.range fun n => ↑n • u n) ⊆ (fun a => ↑f a) ⁻¹' (a • V)
⊢ ↑f (u n) ∈ V
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (↑f '' Set.range fun n => ↑n • u n) ⊆ a • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
⊢ ↑f (u n) ∈ V
simp only [Set.image_subset_iff] at h'
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ↑n • u n ∈ (fun a => ↑f a) ⁻¹' (↑n • V)
⊢ ↑f (u n) ∈ V
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ∀ (a : 𝕜'), r ≤ ‖a‖ → (Set.range fun n => ↑n • u n) ⊆ (fun a => ↑f a) ⁻¹' (a • V)
⊢ ↑f (u n) ∈ V
specialize h' (n : 𝕜') h1 (Set.mem_range_self n)
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ↑n • ↑f (u n) ∈ ↑n • V
⊢ ↑f (u n) ∈ V
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ↑n • u n ∈ (fun a => ↑f a) ⁻¹' (↑n • V)
⊢ ↑f (u n) ∈ V
simp only [Set.mem_preimage, LinearMap.map_smulₛₗ, map_natCast] at h'
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
y : F
hy : y ∈ V
h' : (fun x => ↑n • x) y = ↑n • ↑f (u n)
⊢ ↑f (u n) ∈ V
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ↑n • ↑f (u n) ∈ ↑n • V
⊢ ↑f (u n) ∈ V
rcases h' with ⟨y, hy, h'⟩
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
y : F
hy : y ∈ V
h' : (↑n)⁻¹ • (fun x => ↑n • x) y = (↑n)⁻¹ • ↑n • ↑f (u n)
⊢ ↑f (u n) ∈ V
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
y : F
hy : y ∈ V
h' : (fun x => ↑n • x) y = ↑n • ↑f (u n)
⊢ ↑f (u n) ∈ V
apply_fun fun y : F => (n : 𝕜')⁻¹ • y  at h'
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
y : F
hy : y ∈ V
h' : y = ↑f (u n)
⊢ ↑f (u n) ∈ V
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
y : F
hy : y ∈ V
h' : (↑n)⁻¹ • (fun x => ↑n • x) y = (↑n)⁻¹ • ↑n • ↑f (u n)
⊢ ↑f (u n) ∈ V
simp only [hn', inv_smul_smul₀, Ne.def, Nat.cast_eq_zero, not_false_iff] at h'
no goals
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : IsROrC 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (↑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : HasAntitoneBasis (𝓝 0) fun i => b i
bE' : HasBasis (𝓝 0) (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → ¬↑f (u ia) ∈ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : 0 < r
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
y : F
hy : y ∈ V
h' : y = ↑f (u n)
⊢ ↑f (u n) ∈ V
rwa [← h']