case mp
𝕜 : Type u_2
𝕜₂ : Type u_4
𝕝 : Type ?u.123266
𝕝₂ : Type ?u.123269
E : Type u_3
F : Type u_5
G : Type ?u.123278
ι✝ : Type ?u.123281
ι' : Type u_6
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_1
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : IsBounded (fun x => p) q f
i : ι'
⊢ ∃ C, comp (q i) f ≤ C • p

case mpr
𝕜 : Type u_2
𝕜₂ : Type u_4
𝕝 : Type ?u.123266
𝕝₂ : Type ?u.123269
E : Type u_3
F : Type u_5
G : Type ?u.123278
ι✝ : Type ?u.123281
ι' : Type u_6
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_1
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : ∀ (i : ι'), ∃ C, comp (q i) f ≤ C • p
i : ι'
⊢ ∃ s C, comp (q i) f ≤ C • Finset.sup s fun x => p
𝕜 : Type u_2
𝕜₂ : Type u_4
𝕝 : Type ?u.123266
𝕝₂ : Type ?u.123269
E : Type u_3
F : Type u_5
G : Type ?u.123278
ι✝ : Type ?u.123281
ι' : Type u_6
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_1
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
⊢ IsBounded (fun x => p) q f ↔ ∀ (i : ι'), ∃ C, comp (q i) f ≤ C • p
constructor <;> intro h i
case mpr
𝕜 : Type u_2
𝕜₂ : Type u_4
𝕝 : Type ?u.123266
𝕝₂ : Type ?u.123269
E : Type u_3
F : Type u_5
G : Type ?u.123278
ι✝ : Type ?u.123281
ι' : Type u_6
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_1
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : ∀ (i : ι'), ∃ C, comp (q i) f ≤ C • p
i : ι'
⊢ ∃ C, comp (q i) f ≤ C • Finset.sup {Classical.arbitrary ι} fun x => p
case mpr
𝕜 : Type u_2
𝕜₂ : Type u_4
𝕝 : Type ?u.123266
𝕝₂ : Type ?u.123269
E : Type u_3
F : Type u_5
G : Type ?u.123278
ι✝ : Type ?u.123281
ι' : Type u_6
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_1
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : ∀ (i : ι'), ∃ C, comp (q i) f ≤ C • p
i : ι'
⊢ ∃ s C, comp (q i) f ≤ C • Finset.sup s fun x => p
use {Classical.arbitrary ι}
no goals
case mpr
𝕜 : Type u_2
𝕜₂ : Type u_4
𝕝 : Type ?u.123266
𝕝₂ : Type ?u.123269
E : Type u_3
F : Type u_5
G : Type ?u.123278
ι✝ : Type ?u.123281
ι' : Type u_6
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_1
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : ∀ (i : ι'), ∃ C, comp (q i) f ≤ C • p
i : ι'
⊢ ∃ C, comp (q i) f ≤ C • Finset.sup {Classical.arbitrary ι} fun x => p
simp only [h, Finset.sup_singleton]
case mp.intro.intro
𝕜 : Type u_2
𝕜₂ : Type u_4
𝕝 : Type ?u.123266
𝕝₂ : Type ?u.123269
E : Type u_3
F : Type u_5
G : Type ?u.123278
ι✝ : Type ?u.123281
ι' : Type u_6
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_1
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h✝ : IsBounded (fun x => p) q f
i : ι'
s : Finset ι
C : ℝ≥0
h : comp (q i) f ≤ C • Finset.sup s fun x => p
⊢ ∃ C, comp (q i) f ≤ C • p
case mp
𝕜 : Type u_2
𝕜₂ : Type u_4
𝕝 : Type ?u.123266
𝕝₂ : Type ?u.123269
E : Type u_3
F : Type u_5
G : Type ?u.123278
ι✝ : Type ?u.123281
ι' : Type u_6
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_1
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : IsBounded (fun x => p) q f
i : ι'
⊢ ∃ C, comp (q i) f ≤ C • p
rcases h i with ⟨s, C, h⟩
no goals
case mp.intro.intro
𝕜 : Type u_2
𝕜₂ : Type u_4
𝕝 : Type ?u.123266
𝕝₂ : Type ?u.123269
E : Type u_3
F : Type u_5
G : Type ?u.123278
ι✝ : Type ?u.123281
ι' : Type u_6
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_1
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h✝ : IsBounded (fun x => p) q f
i : ι'
s : Finset ι
C : ℝ≥0
h : comp (q i) f ≤ C • Finset.sup s fun x => p
⊢ ∃ C, comp (q i) f ≤ C • p
exact ⟨C, le_trans h (smul_le_smul (Finset.sup_le fun _ _ => le_rfl) le_rfl)⟩