Theorem: RiemannSphere.continuous_fill (Ray/AnalyticManifold/RiemannSphere.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
⊢ Continuous (fill f y)
Tactic:
rw [continuous_iff_continuousAt]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ (x : 𝕊), ContinuousAt (fill f y) x

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ (x : 𝕊), ContinuousAt (fill f y) x
Tactic:
intro z
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
z : 𝕊
⊢ ContinuousAt (fill f y) z

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
z : 𝕊
⊢ ContinuousAt (fill f y) z
Tactic:
induction z using OnePoint.rec
State after:
case h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fill f y) ∞

case h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
x✝ : ℂ
⊢ ContinuousAt (fill f y) ↑x✝

State before:
case h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fill f y) ∞
Tactic:
exact continuousAt_fill_inf fi
State after:
no goals

State before:
case h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
x✝ : ℂ
⊢ ContinuousAt (fill f y) ↑x✝
Tactic:
exact continuousAt_fill_coe fc.continuousAt
State after:
no goals