X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ContinuousOn (extendFrom A f) univ
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ Continuous (extendFrom A f)
rw [continuous_iff_continuousOn_univ]
no goals
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ContinuousOn (extendFrom A f) univ
exact continuousOn_extendFrom (fun x _ ↦ hA x) (by simpa using hf)
no goals
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ∀ (x : X), x ∈ univ → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
simpa using hf