case intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
val✝ : Fintype ι
⊢ ∃ C, C > 0 ∧ ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
⊢ ∃ C, C > 0 ∧ ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
cases nonempty_fintype ι
no goals
case intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
val✝ : Fintype ι
⊢ ∃ C, C > 0 ∧ ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖↑u (↑v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
exact
  ⟨max (Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊) 1,
    zero_lt_one.trans_le (le_max_right _ _), fun {u} M hu =>
    (v.op_nnnorm_le M hu).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) (zero_le M)⟩