ι : Type u_3
α : Type ?u.452056
X : Type u_1
M : Type u_2
N : Type ?u.452065
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
ι : Type u_3
α : Type ?u.452056
X : Type u_1
M : Type u_2
N : Type ?u.452065
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (i : ι), f i x
refine' continuous_iff_continuousAt.2 fun x => _
case intro
ι : Type u_3
α : Type ?u.452056
X : Type u_1
M : Type u_2
N : Type ?u.452065
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, (∏ᶠ (i : ι), f i y) = ∏ i in s, f i y
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
ι : Type u_3
α : Type ?u.452056
X : Type u_1
M : Type u_2
N : Type ?u.452065
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
rcases finprod_eventually_eq_prod hf x with ⟨s, hs⟩
case intro
ι : Type u_3
α : Type ?u.452056
X : Type u_1
M : Type u_2
N : Type ?u.452065
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, (∏ᶠ (i : ι), f i y) = ∏ i in s, f i y
⊢ ContinuousAt (fun x => ∏ i in s, f i x) x
case intro
ι : Type u_3
α : Type ?u.452056
X : Type u_1
M : Type u_2
N : Type ?u.452065
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, (∏ᶠ (i : ι), f i y) = ∏ i in s, f i y
⊢ ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
refine' ContinuousAt.congr _ (EventuallyEq.symm hs)
no goals
case intro
ι : Type u_3
α : Type ?u.452056
X : Type u_1
M : Type u_2
N : Type ?u.452065
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
x : X
s : Finset ι
hs : ∀ᶠ (y : X) in 𝓝 x, (∏ᶠ (i : ι), f i y) = ∏ i in s, f i y
⊢ ContinuousAt (fun x => ∏ i in s, f i x) x
exact tendsto_finset_prod _ fun i _ => (hc i).continuousAt