case inl
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
⊢ ∃ C s, comp (Finset.sup ∅ q) f ≤ C • Finset.sup s p

case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
s' : Finset ι'
h✝ : Finset.Nonempty s'
⊢ ∃ C s, comp (Finset.sup s' q) f ≤ C • Finset.sup s p
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
s' : Finset ι'
⊢ ∃ C s, comp (Finset.sup s' q) f ≤ C • Finset.sup s p
obtain rfl | _ := s'.eq_empty_or_nonempty
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
⊢ ∃ C s, comp (Finset.sup s' q) f ≤ C • Finset.sup s p
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
s' : Finset ι'
h✝ : Finset.Nonempty s'
⊢ ∃ C s, comp (Finset.sup s' q) f ≤ C • Finset.sup s p
choose fₛ fC hf using hf
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
⊢ comp (Finset.sup s' q) f ≤ (Finset.card s' • Finset.sup s' fC) • Finset.sup (Finset.biUnion s' fₛ) p
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
⊢ ∃ C s, comp (Finset.sup s' q) f ≤ C • Finset.sup s p
use s'.card • s'.sup fC, Finset.biUnion s' fₛ
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
hs : ∀ (i : ι'), i ∈ s' → comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
⊢ comp (Finset.sup s' q) f ≤ (Finset.card s' • Finset.sup s' fC) • Finset.sup (Finset.biUnion s' fₛ) p
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
⊢ comp (Finset.sup s' q) f ≤ (Finset.card s' • Finset.sup s' fC) • Finset.sup (Finset.biUnion s' fₛ) p
have hs : ∀ i : ι', i ∈ s' → (q i).comp f ≤ s'.sup fC • (Finset.biUnion s' fₛ).sup p := by
  intro i hi
  refine' (hf i).trans (smul_le_smul _ (Finset.le_sup hi))
  exact Finset.sup_mono (Finset.subset_biUnion_of_mem fₛ hi)
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
hs : ∀ (i : ι'), i ∈ s' → comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
⊢ comp (∑ i in s', q i) f ≤ (Finset.card s' • Finset.sup s' fC) • Finset.sup (Finset.biUnion s' fₛ) p
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
hs : ∀ (i : ι'), i ∈ s' → comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
⊢ comp (Finset.sup s' q) f ≤ (Finset.card s' • Finset.sup s' fC) • Finset.sup (Finset.biUnion s' fₛ) p
refine' (comp_mono f (finset_sup_le_sum q s')).trans _
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
hs : ∀ (i : ι'), i ∈ s' → comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
⊢ ∑ x in s', comp (q x) f ≤ (Finset.card s' • Finset.sup s' fC) • Finset.sup (Finset.biUnion s' fₛ) p
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
hs : ∀ (i : ι'), i ∈ s' → comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
⊢ comp (∑ i in s', q i) f ≤ (Finset.card s' • Finset.sup s' fC) • Finset.sup (Finset.biUnion s' fₛ) p
simp_rw [← pullback_apply, map_sum, pullback_apply]
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
hs : ∀ (i : ι'), i ∈ s' → comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
⊢ ∑ i in s', Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p ≤
    (Finset.card s' • Finset.sup s' fC) • Finset.sup (Finset.biUnion s' fₛ) p
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
hs : ∀ (i : ι'), i ∈ s' → comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
⊢ ∑ x in s', comp (q x) f ≤ (Finset.card s' • Finset.sup s' fC) • Finset.sup (Finset.biUnion s' fₛ) p
refine' (Finset.sum_le_sum hs).trans _
no goals
case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
hs : ∀ (i : ι'), i ∈ s' → comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
⊢ ∑ i in s', Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p ≤
    (Finset.card s' • Finset.sup s' fC) • Finset.sup (Finset.biUnion s' fₛ) p
rw [Finset.sum_const, smul_assoc]
no goals
case inl
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
⊢ ∃ C s, comp (Finset.sup ∅ q) f ≤ C • Finset.sup s p
exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
no goals
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
⊢ comp (Finset.sup ∅ q) f ≤ 1 • Finset.sup ∅ p
simp [Seminorm.bot_eq_zero]
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
i : ι'
hi : i ∈ s'
⊢ comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
⊢ ∀ (i : ι'), i ∈ s' → comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
intro i hi
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
i : ι'
hi : i ∈ s'
⊢ Finset.sup (fₛ i) p ≤ Finset.sup (Finset.biUnion s' fₛ) p
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
i : ι'
hi : i ∈ s'
⊢ comp (q i) f ≤ Finset.sup s' fC • Finset.sup (Finset.biUnion s' fₛ) p
refine' (hf i).trans (smul_le_smul _ (Finset.le_sup hi))
no goals
𝕜 : Type u_1
𝕜₂ : Type u_3
𝕝 : Type ?u.136429
𝕝₂ : Type ?u.136432
E : Type u_2
F : Type u_4
G : Type ?u.136441
ι : Type u_5
ι' : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : Finset.Nonempty s'
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), comp (q i) f ≤ fC i • Finset.sup (fₛ i) p
i : ι'
hi : i ∈ s'
⊢ Finset.sup (fₛ i) p ≤ Finset.sup (Finset.biUnion s' fₛ) p
exact Finset.sup_mono (Finset.subset_biUnion_of_mem fₛ hi)