Theorem: RiemannSphere.continuous_lift' (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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
⊢ Continuous (uncurry (lift' g ∞))
Tactic:
rw [continuous_iff_continuousOn_univ]
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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
⊢ ContinuousOn (uncurry (lift' g ∞)) univ

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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
⊢ ContinuousOn (uncurry (lift' g ∞)) univ
Tactic:
intro ⟨x, 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✝ : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
z : 𝕊
a✝ : (x, z) ∈ univ
⊢ ContinuousWithinAt (uncurry (lift' g ∞)) univ (x, 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✝ : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
z : 𝕊
a✝ : (x, z) ∈ univ
⊢ ContinuousWithinAt (uncurry (lift' g ∞)) univ (x, z)
Tactic:
apply ContinuousAt.continuousWithinAt
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✝ : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
z : 𝕊
a✝ : (x, z) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, z)

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✝ : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
z : 𝕊
a✝ : (x, z) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, z)
Tactic:
induction z using OnePoint.rec
State after:
case h.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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
a✝ : (x, ∞) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, ∞)

case h.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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
x✝ : ℂ
a✝ : (x, ↑x✝) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, ↑x✝)

State before:
case h.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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
a✝ : (x, ∞) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, ∞)
Tactic:
exact continuousAt_lift_inf' (gi x)
State after:
no goals

State before:
case h.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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
x✝ : ℂ
a✝ : (x, ↑x✝) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, ↑x✝)
Tactic:
exact continuousAt_lift_coe' gc.continuousAt
State after:
no goals