α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.34136
ε : Type ?u.34139
ζ : Type ?u.34142
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
⊢ ∀ (x : α × β), ContinuousAt (uncurry f) x
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.34136
ε : Type ?u.34139
ζ : Type ?u.34142
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
⊢ Continuous (uncurry f)
apply continuous_iff_continuousAt.2
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.34136
ε : Type ?u.34139
ζ : Type ?u.34142
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
a : α
x : β
⊢ ContinuousAt (uncurry f) (a, x)
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.34136
ε : Type ?u.34139
ζ : Type ?u.34142
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
⊢ ∀ (x : α × β), ContinuousAt (uncurry f) x
rintro ⟨a, x⟩
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.34136
ε : Type ?u.34139
ζ : Type ?u.34142
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
a : α
x : β
⊢ map (uncurry f) (𝓝 (a, x)) ≤ 𝓝 (uncurry f (a, x))
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.34136
ε : Type ?u.34139
ζ : Type ?u.34142
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
a : α
x : β
⊢ ContinuousAt (uncurry f) (a, x)
change map _ _ ≤ _
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.34136
ε : Type ?u.34139
ζ : Type ?u.34142
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
a : α
x : β
⊢ map (f a) (𝓝 x) ≤ 𝓝 (uncurry f (a, x))
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.34136
ε : Type ?u.34139
ζ : Type ?u.34142
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
a : α
x : β
⊢ map (uncurry f) (𝓝 (a, x)) ≤ 𝓝 (uncurry f (a, x))
rw [nhds_prod_eq, nhds_discrete, Filter.map_pure_prod]
no goals
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type ?u.34136
ε : Type ?u.34139
ζ : Type ?u.34142
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
inst✝² : TopologicalSpace ε
inst✝¹ : TopologicalSpace ζ
inst✝ : DiscreteTopology α
f : α → β → γ
hf : ∀ (a : α), Continuous (f a)
a : α
x : β
⊢ map (f a) (𝓝 x) ≤ 𝓝 (uncurry f (a, x))
exact (hf a).continuousAt