internlm/Lean-Github huggingface dataset:
Theorem: MDifferentiableAt.hasMFDerivAt_uncurry
Proof state before:
case h
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : N → O → P
y : N
z : O
fd : MDifferentiableAt (J.prod K) L (uncurry f) (y, z)
df0 : TangentSpace J y →L[𝕜] TangentSpace L (f y z)
fh0 : HasMFDerivAt J L (fun x => f x z) y df0
df1 : TangentSpace K z →L[𝕜] TangentSpace L (f y z)
fh1 : HasMFDerivAt K L (fun x => f y x) z df1
fst : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace J y :=
  ContinuousLinearMap.fst 𝕜 (TangentSpace J y) (TangentSpace K z)
snd : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace K z :=
  ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)
df : TangentSpace (J.prod K) (y, z) →L[𝕜] TangentSpace L (uncurry f (y, z))
hdf : mfderiv (J.prod K) L (uncurry f) (y, z) = df
fh : HasMFDerivAt (J.prod K) L (uncurry f) (y, z) df
u : F
v : G
hu : ∀ (u : TangentSpace J y), df (u, 0) = df0 u
hv : ∀ (v : TangentSpace K z), df (0, v) = df1 v
e : (u, v) = (u, 0) + (0, v)
⊢ df (u, 0) + df (0, v) = df0 (fst (u, v)) + df1 (snd (u, v))
Tactic:
exact congr_arg₂ _ (hu u) (hv v)
Proof state after:
no goals
Theorem: MDifferentiableAt.hasMFDerivAt_uncurry
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : N → O → P
y : N
z : O
fd : MDifferentiableAt (J.prod K) L (uncurry f) (y, z)
df0 : TangentSpace J y →L[𝕜] TangentSpace L (f y z)
fh0 : HasMFDerivAt J L (fun x => f x z) y df0
df1 : TangentSpace K z →L[𝕜] TangentSpace L (f y z)
fh1 : HasMFDerivAt K L (fun x => f y x) z df1
fst : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace J y :=
  ContinuousLinearMap.fst 𝕜 (TangentSpace J y) (TangentSpace K z)
snd : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace K z :=
  ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)
df : TangentSpace (J.prod K) (y, z) →L[𝕜] TangentSpace L (uncurry f (y, z))
hdf : mfderiv (J.prod K) L (uncurry f) (y, z) = df
fh : HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)
e : df = df0.comp fst + df1.comp snd
⊢ HasMFDerivAt (J.prod K) L (uncurry f) (y, z) (df0.comp fst + df1.comp snd)
Tactic:
exact fh
Proof state after:
no goals
Theorem: MDifferentiableAt.hasMFDerivAt_uncurry
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : N → O → P
y : N
z : O
fd : MDifferentiableAt (J.prod K) L (uncurry f) (y, z)
df0 : TangentSpace J y →L[𝕜] TangentSpace L (f y z)
fh0 : HasMFDerivAt J L (fun x => f x z) y df0
df1 : TangentSpace K z →L[𝕜] TangentSpace L (f y z)
fh1 : HasMFDerivAt K L (fun x => f y x) z df1
fst : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace J y :=
  ContinuousLinearMap.fst 𝕜 (TangentSpace J y) (TangentSpace K z)
snd : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace K z :=
  ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)
df : TangentSpace (J.prod K) (y, z) →L[𝕜] TangentSpace L (uncurry f (y, z))
hdf : mfderiv (J.prod K) L (uncurry f) (y, z) = df
fh : HasMFDerivAt (J.prod K) L (uncurry f) (y, z) df
u✝ : F
v : G
u : TangentSpace J y
d : HasMFDerivAt J L (uncurry f ∘ fun x => (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0))
⊢ u = (ContinuousLinearMap.id 𝕜 (TangentSpace J y)) u
Tactic:
exact rfl
Proof state after:
no goals
Theorem: MDifferentiableAt.hasMFDerivAt_uncurry
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : N → O → P
y : N
z : O
fd : MDifferentiableAt (J.prod K) L (uncurry f) (y, z)
df0 : TangentSpace J y →L[𝕜] TangentSpace L (f y z)
fh0 : HasMFDerivAt J L (fun x => f x z) y df0
df1 : TangentSpace K z →L[𝕜] TangentSpace L (f y z)
fh1 : HasMFDerivAt K L (fun x => f y x) z df1
fst : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace J y :=
  ContinuousLinearMap.fst 𝕜 (TangentSpace J y) (TangentSpace K z)
snd : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace K z :=
  ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)
df : TangentSpace (J.prod K) (y, z) →L[𝕜] TangentSpace L (uncurry f (y, z))
hdf : mfderiv (J.prod K) L (uncurry f) (y, z) = df
fh : HasMFDerivAt (J.prod K) L (uncurry f) (y, z) df
u : F
v✝ : G
hu : ∀ (u : TangentSpace J y), df (u, 0) = df0 u
v : TangentSpace K z
d :
  HasMFDerivAt K L (uncurry f ∘ fun x => (y, x)) z
    (df.comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 (TangentSpace K z))))
⊢ 0 = 0 v ∧ v = (ContinuousLinearMap.id 𝕜 (TangentSpace K z)) v
Tactic:
exact ⟨(ContinuousLinearMap.zero_apply _).symm, rfl⟩
Proof state after:
no goals
Theorem: MDifferentiableAt.hasMFDerivAt_uncurry
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : N → O → P
y : N
z : O
fd : MDifferentiableAt (J.prod K) L (uncurry f) (y, z)
df0 : TangentSpace J y →L[𝕜] TangentSpace L (f y z)
fh0 : HasMFDerivAt J L (fun x => f x z) y df0
df1 : TangentSpace K z →L[𝕜] TangentSpace L (f y z)
fh1 : HasMFDerivAt K L (fun x => f y x) z df1
fst : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace J y :=
  ContinuousLinearMap.fst 𝕜 (TangentSpace J y) (TangentSpace K z)
snd : TangentSpace J y × TangentSpace K z →L[𝕜] TangentSpace K z :=
  ContinuousLinearMap.snd 𝕜 (TangentSpace J y) (TangentSpace K z)
df : TangentSpace (J.prod K) (y, z) →L[𝕜] TangentSpace L (uncurry f (y, z))
hdf : mfderiv (J.prod K) L (uncurry f) (y, z) = df
fh : HasMFDerivAt (J.prod K) L (uncurry f) (y, z) df
u : F
v : G
hu : ∀ (u : TangentSpace J y), df (u, 0) = df0 u
hv : ∀ (v : TangentSpace K z), df (0, v) = df1 v
⊢ (u, v) = (u, 0) + (0, v)
Tactic:
simp only [Prod.mk_add_mk, add_zero, zero_add]
Proof state after:
no goals
Theorem: MDifferentiableAt.hasMFDerivAt_comp2
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : N → O → P
g : M → N
h : M → O
x : M
fd : MDifferentiableAt (J.prod K) L (uncurry f) (g x, h x)
dg : TangentSpace I x →L[𝕜] TangentSpace J (g x)
gh : HasMFDerivAt I J g x dg
dh : TangentSpace I x →L[𝕜] TangentSpace K (h x)
hh : HasMFDerivAt I K h x dh
df0 : TangentSpace J (g x) →L[𝕜] TangentSpace L (f (g x) (h x))
fh0 : HasMFDerivAt J L (fun y => f y (h x)) (g x) df0
df1 : TangentSpace K (h x) →L[𝕜] TangentSpace L (f (g x) (h x))
fh1 : HasMFDerivAt K L (fun y => f (g x) y) (h x) df1
fh :
  HasMFDerivAt I L (uncurry f ∘ fun y => (g y, h y)) x
    (df0.comp ((ContinuousLinearMap.fst 𝕜 (TangentSpace J (g x)) (TangentSpace K (h x))).comp (dg.prod dh)) +
      df1.comp ((ContinuousLinearMap.snd 𝕜 (TangentSpace J (g x)) (TangentSpace K (h x))).comp (dg.prod dh)))
⊢ HasMFDerivAt I L (fun y => f (g y) (h y)) x (df0.comp dg + df1.comp dh)
Tactic:
exact fh
Proof state after:
no goals
Theorem: hasMFDerivAt_iff_hasFDerivAt'
Proof state before:
𝕜 : Type
inst✝³⁴ : NontriviallyNormedField 𝕜
E A : Type
inst✝³³ : NormedAddCommGroup E
inst✝³² : NormedSpace 𝕜 E
inst✝³¹ : CompleteSpace E
inst✝³⁰ : TopologicalSpace A
F B : Type
inst✝²⁹ : NormedAddCommGroup F
inst✝²⁸ : NormedSpace 𝕜 F
inst✝²⁷ : CompleteSpace F
inst✝²⁶ : TopologicalSpace B
G C : Type
inst✝²⁵ : NormedAddCommGroup G
inst✝²⁴ : NormedSpace 𝕜 G
inst✝²³ : TopologicalSpace C
H D : Type
inst✝²² : NormedAddCommGroup H
inst✝²¹ : NormedSpace 𝕜 H
inst✝²⁰ : TopologicalSpace D
M : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹⁹ : TopologicalSpace M
N : Type
J✝ : ModelWithCorners 𝕜 F B
inst✝¹⁸ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁷ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁶ : TopologicalSpace P
inst✝¹⁵ : I✝.Boundaryless
inst✝¹⁴ : ChartedSpace A M
cm : AnalyticManifold I✝ M
inst✝¹³ : J✝.Boundaryless
inst✝¹² : ChartedSpace B N
cn : AnalyticManifold J✝ N
inst✝¹¹ : K.Boundaryless
inst✝¹⁰ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁹ : L.Boundaryless
inst✝⁸ : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A E
inst✝⁵ : AnalyticManifold I E
inst✝⁴ : ExtChartEqRefl I
J : ModelWithCorners 𝕜 F B
inst✝³ : J.Boundaryless
inst✝² : ChartedSpace B F
inst✝¹ : AnalyticManifold J F
inst✝ : ExtChartEqRefl J
f : E → F
x : E
f' : E →L[𝕜] F
⊢ HasMFDerivAt I J f x f' ↔ HasFDerivAt f f' x
Tactic:
simp only [HasMFDerivAt, ModelWithCorners.range_eq_univ, hasFDerivWithinAt_univ,
  writtenInExtChartAt, extChartAt_eq_refl, Function.comp, PartialEquiv.refl_coe,
  PartialEquiv.refl_symm, id]
Proof state after:
𝕜 : Type
inst✝³⁴ : NontriviallyNormedField 𝕜
E A : Type
inst✝³³ : NormedAddCommGroup E
inst✝³² : NormedSpace 𝕜 E
inst✝³¹ : CompleteSpace E
inst✝³⁰ : TopologicalSpace A
F B : Type
inst✝²⁹ : NormedAddCommGroup F
inst✝²⁸ : NormedSpace 𝕜 F
inst✝²⁷ : CompleteSpace F
inst✝²⁶ : TopologicalSpace B
G C : Type
inst✝²⁵ : NormedAddCommGroup G
inst✝²⁴ : NormedSpace 𝕜 G
inst✝²³ : TopologicalSpace C
H D : Type
inst✝²² : NormedAddCommGroup H
inst✝²¹ : NormedSpace 𝕜 H
inst✝²⁰ : TopologicalSpace D
M : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹⁹ : TopologicalSpace M
N : Type
J✝ : ModelWithCorners 𝕜 F B
inst✝¹⁸ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁷ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁶ : TopologicalSpace P
inst✝¹⁵ : I✝.Boundaryless
inst✝¹⁴ : ChartedSpace A M
cm : AnalyticManifold I✝ M
inst✝¹³ : J✝.Boundaryless
inst✝¹² : ChartedSpace B N
cn : AnalyticManifold J✝ N
inst✝¹¹ : K.Boundaryless
inst✝¹⁰ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁹ : L.Boundaryless
inst✝⁸ : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A E
inst✝⁵ : AnalyticManifold I E
inst✝⁴ : ExtChartEqRefl I
J : ModelWithCorners 𝕜 F B
inst✝³ : J.Boundaryless
inst✝² : ChartedSpace B F
inst✝¹ : AnalyticManifold J F
inst✝ : ExtChartEqRefl J
f : E → F
x : E
f' : E →L[𝕜] F
⊢ ContinuousAt f x ∧ HasFDerivAt (fun x => f x) f' x ↔ HasFDerivAt f f' x
Theorem: hasMFDerivAt_iff_hasFDerivAt'
Proof state before:
𝕜 : Type
inst✝³⁴ : NontriviallyNormedField 𝕜
E A : Type
inst✝³³ : NormedAddCommGroup E
inst✝³² : NormedSpace 𝕜 E
inst✝³¹ : CompleteSpace E
inst✝³⁰ : TopologicalSpace A
F B : Type
inst✝²⁹ : NormedAddCommGroup F
inst✝²⁸ : NormedSpace 𝕜 F
inst✝²⁷ : CompleteSpace F
inst✝²⁶ : TopologicalSpace B
G C : Type
inst✝²⁵ : NormedAddCommGroup G
inst✝²⁴ : NormedSpace 𝕜 G
inst✝²³ : TopologicalSpace C
H D : Type
inst✝²² : NormedAddCommGroup H
inst✝²¹ : NormedSpace 𝕜 H
inst✝²⁰ : TopologicalSpace D
M : Type
I✝ : ModelWithCorners 𝕜 E A
inst✝¹⁹ : TopologicalSpace M
N : Type
J✝ : ModelWithCorners 𝕜 F B
inst✝¹⁸ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁷ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹⁶ : TopologicalSpace P
inst✝¹⁵ : I✝.Boundaryless
inst✝¹⁴ : ChartedSpace A M
cm : AnalyticManifold I✝ M
inst✝¹³ : J✝.Boundaryless
inst✝¹² : ChartedSpace B N
cn : AnalyticManifold J✝ N
inst✝¹¹ : K.Boundaryless
inst✝¹⁰ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁹ : L.Boundaryless
inst✝⁸ : ChartedSpace D P
cp : AnalyticManifold L P
I : ModelWithCorners 𝕜 E A
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A E
inst✝⁵ : AnalyticManifold I E
inst✝⁴ : ExtChartEqRefl I
J : ModelWithCorners 𝕜 F B
inst✝³ : J.Boundaryless
inst✝² : ChartedSpace B F
inst✝¹ : AnalyticManifold J F
inst✝ : ExtChartEqRefl J
f : E → F
x : E
f' : E →L[𝕜] F
⊢ ContinuousAt f x ∧ HasFDerivAt (fun x => f x) f' x ↔ HasFDerivAt f f' x
Tactic:
exact ⟨fun x ↦ x.2, fun d ↦ ⟨d.continuousAt, d⟩⟩
Proof state after:
no goals
Theorem: HolomorphicOn.continuousOn_tangentMap
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
s : Set M
fa : HolomorphicOn I J f s
⊢ ContinuousOn (tangentMap I J f) (Bundle.TotalSpace.proj ⁻¹' s)
Tactic:
generalize ht : {x | HolomorphicAt I J f x} = t
Proof state after:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
s : Set M
fa : HolomorphicOn I J f s
t : Set M
ht : {x | HolomorphicAt I J f x} = t
⊢ ContinuousOn (tangentMap I J f) (Bundle.TotalSpace.proj ⁻¹' s)
Theorem: HolomorphicOn.continuousOn_tangentMap
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
s : Set M
fa : HolomorphicOn I J f s
t : Set M
ht : {x | HolomorphicAt I J f x} = t
⊢ ContinuousOn (tangentMap I J f) (Bundle.TotalSpace.proj ⁻¹' s)
Tactic:
have o : IsOpen t := by rw [← ht]; exact isOpen_holomorphicAt
Proof state after:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
s : Set M
fa : HolomorphicOn I J f s
t : Set M
ht : {x | HolomorphicAt I J f x} = t
o : IsOpen t
⊢ ContinuousOn (tangentMap I J f) (Bundle.TotalSpace.proj ⁻¹' s)