𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
i : ι'
⊢ ContinuousAt (↑(comp (q i) f)) 0
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
⊢ Continuous ↑f
refine' continuous_of_continuous_comp hq _ fun i => Seminorm.continuous_of_continuousAt_zero _
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
i : ι'
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : E) in 𝓝 0, dist (↑(comp (q i) f) x) 0 < ε
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
i : ι'
⊢ ContinuousAt (↑(comp (q i) f)) 0
rw [Metric.continuousAt_iff', map_zero]
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
⊢ ∀ᶠ (x : E) in 𝓝 0, dist (↑(comp (q i) f) x) 0 < r
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
i : ι'
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : E) in 𝓝 0, dist (↑(comp (q i) f) x) 0 < ε
intro r hr
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
⊢ ∀ᶠ (x : E) in 𝓝 0, dist (↑(comp (q i) f) x) 0 < r
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
⊢ ∀ᶠ (x : E) in 𝓝 0, dist (↑(comp (q i) f) x) 0 < r
rcases hf i with ⟨s₁, C, hf⟩
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ ∀ᶠ (x : E) in 𝓝 0, dist (↑(comp (q i) f) x) 0 < r
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
⊢ ∀ᶠ (x : E) in 𝓝 0, dist (↑(comp (q i) f) x) 0 < r
have hC' : 0 < C + 1 := by positivity
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ ∃ i_1, i_1 ∈ SeminormFamily.basisSets p ∧ ∀ ⦃x : E⦄, x ∈ id i_1 → dist (↑(comp (q i) f) x) 0 < r
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ ∀ᶠ (x : E) in 𝓝 0, dist (↑(comp (q i) f) x) 0 < r
rw [hp.hasBasis.eventually_iff]
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ ∀ ⦃x : E⦄, x ∈ id (ball (Finset.sup s₁ p) 0 (r / (↑C + 1))) → dist (↑(comp (q i) f) x) 0 < r
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ ∃ i_1, i_1 ∈ SeminormFamily.basisSets p ∧ ∀ ⦃x : E⦄, x ∈ id i_1 → dist (↑(comp (q i) f) x) 0 < r
refine' ⟨(s₁.sup p).ball 0 (r / (C + 1)), p.basisSets_mem _ (div_pos hr (by norm_cast)), _⟩
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ ∀ ⦃x : E⦄, x ∈ id (ball (Finset.sup s₁ p) 0 (r / (↑C + 1))) → x ∈ ball (comp (q i) f) 0 r
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ ∀ ⦃x : E⦄, x ∈ id (ball (Finset.sup s₁ p) 0 (r / (↑C + 1))) → dist (↑(comp (q i) f) x) 0 < r
simp_rw [← Metric.mem_ball, ← mem_preimage, ← ball_zero_eq_preimage_ball]
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ id (ball (Finset.sup s₁ p) 0 (r / (↑C + 1))) ⊆ ball (C • Finset.sup s₁ p) 0 r
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ ∀ ⦃x : E⦄, x ∈ id (ball (Finset.sup s₁ p) 0 (r / (↑C + 1))) → x ∈ ball (comp (q i) f) 0 r
refine' Subset.trans _ (ball_antitone hf)
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ id (ball (Finset.sup s₁ p) 0 (r / ↑(C + 1))) ⊆ ball (C • Finset.sup s₁ p) 0 r
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ id (ball (Finset.sup s₁ p) 0 (r / (↑C + 1))) ⊆ ball (C • Finset.sup s₁ p) 0 r
norm_cast
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ id (ball ((C + 1) • Finset.sup s₁ p) 0 r) ⊆ ball (C • Finset.sup s₁ p) 0 r
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ id (ball (Finset.sup s₁ p) 0 (r / ↑(C + 1))) ⊆ ball (C • Finset.sup s₁ p) 0 r
rw [← ball_smul (s₁.sup p) hC']
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ C ≤ C + 1
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ id (ball ((C + 1) • Finset.sup s₁ p) 0 r) ⊆ ball (C • Finset.sup s₁ p) 0 r
refine' ball_antitone (smul_le_smul le_rfl _)
no goals
case intro.intro
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ C ≤ C + 1
simp only [le_add_iff_nonneg_right, zero_le']
no goals
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
⊢ 0 < C + 1
positivity
no goals
𝕜 : Type ?u.555943
𝕜₂ : Type ?u.555946
𝕝 : Type u_1
𝕝₂ : Type u_4
E : Type u_2
F : Type u_5
G : Type ?u.555961
ι : Type u_3
ι' : Type u_6
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
hp : WithSeminorms p
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf✝ : IsBounded p q f
i : ι'
r : ℝ
hr : r > 0
s₁ : Finset ι
C : ℝ≥0
hf : comp (q i) f ≤ C • Finset.sup s₁ p
hC' : 0 < C + 1
⊢ 0 < ↑C + 1
norm_cast