α : Type ?u.138674
β : Type ?u.138677
γ : Type ?u.138680
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
ι' : Sort u_2
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0∞
g : ι' → ℝ≥0∞
a : ℝ≥0∞
h : ∀ (i : ι) (j : ι'), f i + g j ≤ a
⊢ (⨆ (b : ι) (b_1 : ι'), f b + g b_1) ≤ a
α : Type ?u.138674
β : Type ?u.138677
γ : Type ?u.138680
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
ι' : Sort u_2
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0∞
g : ι' → ℝ≥0∞
a : ℝ≥0∞
h : ∀ (i : ι) (j : ι'), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a
simp_rw [iSup_add, add_iSup]
no goals
α : Type ?u.138674
β : Type ?u.138677
γ : Type ?u.138680
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
ι' : Sort u_2
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0∞
g : ι' → ℝ≥0∞
a : ℝ≥0∞
h : ∀ (i : ι) (j : ι'), f i + g j ≤ a
⊢ (⨆ (b : ι) (b_1 : ι'), f b + g b_1) ≤ a
exact iSup₂_le h