case intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
⊢ Bounded (s * t)
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
⊢ Bounded (s * t)
obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le'
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
⊢ Bounded (s * t)
case intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
⊢ Bounded (s * t)
obtain ⟨Rt, hRt⟩ : ∃ R, ∀ x ∈ t, ‖x‖ ≤ R := ht.exists_norm_le'
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
⊢ ∀ (x : E), x ∈ s * t → ‖x‖ ≤ Rs + Rt
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
⊢ Bounded (s * t)
refine' bounded_iff_forall_norm_le'.2 ⟨Rs + Rt, _⟩
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x✝ y✝ : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
x y : E
hx : x ∈ s
hy : y ∈ t
⊢ ‖(fun x x_1 => x * x_1) x y‖ ≤ Rs + Rt
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
⊢ ∀ (x : E), x ∈ s * t → ‖x‖ ≤ Rs + Rt
rintro z ⟨x, y, hx, hy, rfl⟩
no goals
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x✝ y✝ : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
x y : E
hx : x ∈ s
hy : y ∈ t
⊢ ‖(fun x x_1 => x * x_1) x y‖ ≤ Rs + Rt
exact norm_mul_le_of_le (hRs x hx) (hRt y hy)