𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
⊢ IsSeqClosed ↑(graph g)
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
⊢ Continuous ↑g
refine' g.continuous_of_isClosed_graph (IsSeqClosed.isClosed _)
case mk
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
⊢ (x, y) ∈ ↑(graph g)
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
⊢ IsSeqClosed ↑(graph g)
rintro φ ⟨x, y⟩ hφg hφ
case mk
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
⊢ Tendsto (↑g ∘ Prod.fst ∘ φ) atTop (𝓝 y)
case mk
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
⊢ (x, y) ∈ ↑(graph g)
refine' hg (Prod.fst ∘ φ) x y ((continuous_fst.tendsto _).comp hφ) _
case mk
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
this : ↑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
⊢ Tendsto (↑g ∘ Prod.fst ∘ φ) atTop (𝓝 y)
case mk
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
⊢ Tendsto (↑g ∘ Prod.fst ∘ φ) atTop (𝓝 y)
have : g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ := by
  ext n
  exact (hφg n).symm
case mk
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
this : ↑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
⊢ Tendsto (Prod.snd ∘ φ) atTop (𝓝 y)
case mk
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
this : ↑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
⊢ Tendsto (↑g ∘ Prod.fst ∘ φ) atTop (𝓝 y)
rw [this]
no goals
case mk
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
this : ↑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
⊢ Tendsto (Prod.snd ∘ φ) atTop (𝓝 y)
exact (continuous_snd.tendsto _).comp hφ
case h
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
n : ℕ
⊢ (↑g ∘ Prod.fst ∘ φ) n = (Prod.snd ∘ φ) n
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
⊢ ↑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
ext n
no goals
case h
𝕜 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (↑g ∘ u) atTop (𝓝 y) → y = ↑g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑(graph g)
hφ : Tendsto φ atTop (𝓝 (x, y))
n : ℕ
⊢ (↑g ∘ Prod.fst ∘ φ) n = (Prod.snd ∘ φ) n
exact (hφg n).symm