E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
h' : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
⊢ (⨆ (i : ι), ↑‖g i‖₊) < ⊤
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
⊢ (⨆ (i : ι), ↑‖g i‖₊) < ⊤
have h' : ∀ x : E, ∃ C : ℝ, ∀ i : ι, ‖g i x‖ ≤ C := by
  intro x
  rcases lt_iff_exists_coe.mp (h x) with ⟨p, hp₁, _⟩
  refine' ⟨p, fun i => _⟩
  exact_mod_cast
    calc
      (‖g i x‖₊ : ℝ≥0∞) ≤ ⨆ j, ↑‖g j x‖₊ := le_iSup (fun j => (‖g j x‖₊ : ℝ≥0∞)) i
      _ = p := hp₁
case intro
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
h' : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
C' : ℝ
hC' : ∀ (i : ι), ‖g i‖ ≤ C'
⊢ (⨆ (i : ι), ↑‖g i‖₊) < ⊤
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
h' : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
⊢ (⨆ (i : ι), ↑‖g i‖₊) < ⊤
cases' banach_steinhaus h' with C' hC'
case intro
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
h' : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
C' : ℝ
hC' : ∀ (i : ι), ‖g i‖ ≤ C'
i : ι
⊢ ↑‖g i‖₊ ≤ ↑(Real.toNNReal C')
case intro
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
h' : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
C' : ℝ
hC' : ∀ (i : ι), ‖g i‖ ≤ C'
⊢ (⨆ (i : ι), ↑‖g i‖₊) < ⊤
refine' (iSup_le fun i => _).trans_lt (@coe_lt_top C'.toNNReal)
case intro
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
h' : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
C' : ℝ
hC' : ∀ (i : ι), ‖g i‖ ≤ C'
i : ι
⊢ ↑(Real.toNNReal ‖g i‖) ≤ ↑(Real.toNNReal C')
case intro
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
h' : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
C' : ℝ
hC' : ∀ (i : ι), ‖g i‖ ≤ C'
i : ι
⊢ ↑‖g i‖₊ ≤ ↑(Real.toNNReal C')
rw [← norm_toNNReal]
no goals
case intro
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
h' : ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
C' : ℝ
hC' : ∀ (i : ι), ‖g i‖ ≤ C'
i : ι
⊢ ↑(Real.toNNReal ‖g i‖) ≤ ↑(Real.toNNReal C')
exact coe_mono (Real.toNNReal_le_toNNReal <| hC' i)
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
x : E
⊢ ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
⊢ ∀ (x : E), ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
intro x
case intro.intro
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
x : E
p : NNReal
hp₁ : (⨆ (i : ι), ↑‖↑(g i) x‖₊) = ↑p
right✝ : ↑p < ⊤
⊢ ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
x : E
⊢ ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
rcases lt_iff_exists_coe.mp (h x) with ⟨p, hp₁, _⟩
case intro.intro
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
x : E
p : NNReal
hp₁ : (⨆ (i : ι), ↑‖↑(g i) x‖₊) = ↑p
right✝ : ↑p < ⊤
i : ι
⊢ ‖↑(g i) x‖ ≤ ↑p
case intro.intro
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
x : E
p : NNReal
hp₁ : (⨆ (i : ι), ↑‖↑(g i) x‖₊) = ↑p
right✝ : ↑p < ⊤
⊢ ∃ C, ∀ (i : ι), ‖↑(g i) x‖ ≤ C
refine' ⟨p, fun i => _⟩
no goals
case intro.intro
E : Type u_2
F : Type u_5
𝕜 : 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_1
inst✝ : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), (⨆ (i : ι), ↑‖↑(g i) x‖₊) < ⊤
x : E
p : NNReal
hp₁ : (⨆ (i : ι), ↑‖↑(g i) x‖₊) = ↑p
right✝ : ↑p < ⊤
i : ι
⊢ ‖↑(g i) x‖ ≤ ↑p
exact_mod_cast
  calc
    (‖g i x‖₊ : ℝ≥0∞) ≤ ⨆ j, ↑‖g j x‖₊ := le_iSup (fun j => (‖g j x‖₊ : ℝ≥0∞)) i
    _ = p := hp₁