case pos
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ a * iSup f = ⨆ (i : ι), a * f i

case neg
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ a * iSup f = ⨆ (i : ι), a * f i
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a * iSup f = ⨆ (i : ι), a * f i
by_cases hf : ∀ i, f i = 0
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ f = fun x => 0

case pos
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
a : ℝ≥0∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ (a * ⨆ (x : ι), 0) = ⨆ (i : ι), a * (fun x => 0) i
case pos
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ a * iSup f = ⨆ (i : ι), a * f i
obtain rfl : f = fun _ => 0
case pos
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
a : ℝ≥0∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ (a * ⨆ (x : ι), 0) = ⨆ (i : ι), a * (fun x => 0) i
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ f = fun x => 0

case pos
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
a : ℝ≥0∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ (a * ⨆ (x : ι), 0) = ⨆ (i : ι), a * (fun x => 0) i
exact funext hf
no goals
case pos
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
a : ℝ≥0∞
hf : ∀ (i : ι), (fun x => 0) i = 0
⊢ (a * ⨆ (x : ι), 0) = ⨆ (i : ι), a * (fun x => 0) i
simp only [iSup_zero_eq_zero, mul_zero]
case neg
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ ContinuousAt (fun x => a * id x) (⨆ (i : ι), f i)
case neg
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ a * iSup f = ⨆ (i : ι), a * f i
refine' (monotone_id.const_mul' _).map_iSup_of_continuousAt _ (mul_zero a)
case neg
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ id (⨆ (i : ι), f i) ≠ 0
case neg
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ ContinuousAt (fun x => a * id x) (⨆ (i : ι), f i)
refine' ENNReal.Tendsto.const_mul tendsto_id (Or.inl _)
no goals
case neg
α : Type ?u.153814
β : Type ?u.153817
γ : Type ?u.153820
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ id (⨆ (i : ι), f i) ≠ 0
exact mt iSup_eq_zero.1 hf