[GOAL]
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
⊢ ∃ C', ∀ (i : ι), ‖g i‖ ≤ C'
[PROOFSTEP]
rw [show (∃ C, ∀ i, ‖g i‖ ≤ C) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 5 2]
[GOAL]
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
⊢ UniformEquicontinuous (FunLike.coe ∘ g)
[PROOFSTEP]
refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)
[GOAL]
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
x✝ : Fin 1
x : E
⊢ BddAbove (range fun i => ↑(normSeminorm 𝕜₂ F) (↑(g i) x))
[PROOFSTEP]
simpa [bddAbove_def, forall_range_iff] using h x
[GOAL]
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ⨆ (i : ι), ↑‖↑(g i) x‖₊ < ⊤
⊢ ⨆ (i : ι), ↑‖g i‖₊ < ⊤
[PROOFSTEP]
rw [show ((⨆ i, ↑‖g i‖₊) < ∞) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 8 2]
[GOAL]
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ⨆ (i : ι), ↑‖↑(g i) x‖₊ < ⊤
⊢ UniformEquicontinuous (FunLike.coe ∘ g)
[PROOFSTEP]
refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)
[GOAL]
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_5
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ⨆ (i : ι), ↑‖↑(g i) x‖₊ < ⊤
x✝ : Fin 1
x : E
⊢ BddAbove (range fun i => ↑(normSeminorm 𝕜₂ F) (↑(g i) x))
[PROOFSTEP]
simpa [← NNReal.bddAbove_coe, ← Set.range_comp] using (WithTop.iSup_coe_lt_top (fun i ↦ ‖g i x‖₊)).mp (h x)
