ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAlgebra 𝕜 R<VAR>m : ℕ∞<GOAL>ContMDiff 𝓘(𝕜, R) 𝓘(𝕜, R) m Units.val
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>h : IsConnected s<GOAL>s.Nonempty
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>h : IsConnected s<GOAL>IsPreconnected s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>H : IsPreirreducible s<GOAL>IsPreconnected s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>H : IsIrreducible s<GOAL>IsConnected s
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>IsPreconnected ∅
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>IsConnected {x}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>IsPreconnected {x}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>IsPreconnected s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>x : α<VAR>H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t<GOAL>IsPreconnected s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t<GOAL>IsPreconnected s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>c : Set (Set α)<VAR>H1 : ∀ s ∈ c, x ∈ s<VAR>H2 : ∀ s ∈ c, IsPreconnected s<GOAL>IsPreconnected (⋃₀ c)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>ι : Sort u_3<VAR>s : ι → Set α<VAR>h₁ : (⋂ i, s i).Nonempty<VAR>h₂ : ∀ (i : ι), IsPreconnected (s i)<GOAL>IsPreconnected (⋃ i, s i)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>s t : Set α<VAR>H1 : x ∈ s<VAR>H2 : x ∈ t<VAR>H3 : IsPreconnected s<VAR>H4 : IsPreconnected t<GOAL>IsPreconnected (s ∪ t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>H : (s ∩ t).Nonempty<VAR>hs : IsPreconnected s<VAR>ht : IsPreconnected t<GOAL>IsPreconnected (s ∪ t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>H : (s ∩ t).Nonempty<VAR>Hs : IsConnected s<VAR>Ht : IsConnected t<GOAL>IsConnected (s ∪ t)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>S : Set (Set α)<VAR>K : DirectedOn (fun x x_1 => x ⊆ x_1) S<VAR>H : ∀ s ∈ S, IsPreconnected s<GOAL>IsPreconnected (⋃₀ S)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>ι : Type u_3<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ t, IsPreconnected (s i)<VAR>K : ∀ i ∈ t, ∀ j ∈ t, Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j<GOAL>IsPreconnected (⋃ n ∈ t, s n)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>ι : Type u_3<VAR>t : Set ι<VAR>s : ι → Set α<VAR>ht : t.Nonempty<VAR>H : ∀ i ∈ t, IsConnected (s i)<VAR>K : ∀ i ∈ t, ∀ j ∈ t, Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j<GOAL>IsConnected (⋃ n ∈ t, s n)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>ι : Type u_3<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsPreconnected (s i)<VAR>K : ∀ (i j : ι), Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j<GOAL>IsPreconnected (⋃ n, s n)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>ι : Type u_3<VAR>Nonempty ι<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsConnected (s i)<VAR>K : ∀ (i j : ι), Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j<GOAL>IsConnected (⋃ n, s n)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>SuccOrder β<VAR>IsSuccArchimedean β<VAR>s : β → Set α<VAR>H : ∀ (n : β), IsPreconnected (s n)<VAR>K : ∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty<GOAL>IsPreconnected (⋃ n, s n)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>SuccOrder β<VAR>IsSuccArchimedean β<VAR>Nonempty β<VAR>s : β → Set α<VAR>H : ∀ (n : β), IsConnected (s n)<VAR>K : ∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty<GOAL>IsConnected (⋃ n, s n)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>SuccOrder β<VAR>IsSuccArchimedean β<VAR>s : β → Set α<VAR>t : Set β<VAR>ht : t.OrdConnected<VAR>H : ∀ n ∈ t, IsPreconnected (s n)<VAR>K : ∀ n ∈ t, Order.succ n ∈ t → (s n ∩ s (Order.succ n)).Nonempty<GOAL>IsPreconnected (⋃ n ∈ t, s n)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>SuccOrder β<VAR>IsSuccArchimedean β<VAR>s : β → Set α<VAR>t : Set β<VAR>hnt : t.Nonempty<VAR>ht : t.OrdConnected<VAR>H : ∀ n ∈ t, IsConnected (s n)<VAR>K : ∀ n ∈ t, Order.succ n ∈ t → (s n ∩ s (Order.succ n)).Nonempty<GOAL>IsConnected (⋃ n ∈ t, s n)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>H : IsPreconnected s<VAR>Kst : s ⊆ t<VAR>Ktcs : t ⊆ closure s<GOAL>IsPreconnected t
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>H : IsConnected s<VAR>Kst : s ⊆ t<VAR>Ktcs : t ⊆ closure s<GOAL>IsConnected t
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>H : IsPreconnected s<GOAL>IsPreconnected (closure s)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>H : IsConnected s<GOAL>IsConnected (closure s)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>H : IsPreconnected s<VAR>f : α → β<VAR>hf : ContinuousOn f s<GOAL>IsPreconnected (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>H : IsConnected s<VAR>f : α → β<VAR>hf : ContinuousOn f s<GOAL>IsConnected (f '' s)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>IsPreconnected s ↔ ∀ (t t' : Set α), IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Inducing f<GOAL>IsPreconnected (f '' s) ↔ IsPreconnected s
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>hs : IsPreconnected s<VAR>hinj : Function.Injective f<VAR>hf : IsOpenMap f<VAR>hsf : s ⊆ Set.range f<GOAL>IsPreconnected (f ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set β<VAR>hs : IsPreconnected s<VAR>f : α → β<VAR>hinj : Function.Injective f<VAR>hf : IsClosedMap f<VAR>hsf : s ⊆ Set.range f<GOAL>IsPreconnected (f ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set β<VAR>hs : IsConnected s<VAR>f : α → β<VAR>hinj : Function.Injective f<VAR>hf : IsOpenMap f<VAR>hsf : s ⊆ Set.range f<GOAL>IsConnected (f ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set β<VAR>hs : IsConnected s<VAR>f : α → β<VAR>hinj : Function.Injective f<VAR>hf : IsClosedMap f<VAR>hsf : s ⊆ Set.range f<GOAL>IsConnected (f ⁻¹' s)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : Disjoint u v<VAR>hsuv : s ⊆ u ∪ v<VAR>hs : IsPreconnected s<GOAL>s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : Disjoint u v<VAR>hsuv : s ⊆ u ∪ v<VAR>hsu : (s ∩ u).Nonempty<VAR>hs : IsPreconnected s<GOAL>s ⊆ u
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : Disjoint u v<VAR>hsuv : s ⊆ u ∪ v<VAR>hsv : (s ∩ v).Nonempty<VAR>hs : IsPreconnected s<GOAL>s ⊆ v
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s u : Set α<VAR>hs : IsPreconnected s<VAR>hu : IsOpen u<VAR>h'u : (s ∩ u).Nonempty<VAR>h : closure u ∩ s ⊆ u<GOAL>s ⊆ u
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>t : Set β<VAR>hs : IsPreconnected s<VAR>ht : IsPreconnected t<GOAL>IsPreconnected (s ×ˢ t)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>t : Set β<VAR>hs : IsConnected s<VAR>ht : IsConnected t<GOAL>IsConnected (s ×ˢ t)
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (π i)<VAR>s : (i : ι) → Set (π i)<VAR>hs : ∀ (i : ι), IsPreconnected (s i)<GOAL>IsPreconnected (Set.univ.pi s)
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (π i)<VAR>s : (i : ι) → Set (π i)<GOAL>IsConnected (Set.univ.pi s) ↔ ∀ (i : ι), IsConnected (s i)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>F : Set α<VAR>x : α<VAR>h : x ∈ F<GOAL>connectedComponentIn F x = Subtype.val '' connectedComponent ⟨x, h⟩
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>F : Set α<VAR>x : α<VAR>h : x ∉ F<GOAL>connectedComponentIn F x = ∅
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>x ∈ connectedComponent x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>F : Set α<VAR>hx : x ∈ F<GOAL>x ∈ connectedComponentIn F x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>(connectedComponent x).Nonempty
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>F : Set α<GOAL>(connectedComponentIn F x).Nonempty ↔ x ∈ F
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>F : Set α<VAR>x : α<GOAL>connectedComponentIn F x ⊆ F
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>IsPreconnected (connectedComponent x)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>F : Set α<GOAL>IsPreconnected (connectedComponentIn F x)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>IsConnected (connectedComponent x)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>F : Set α<GOAL>IsConnected (connectedComponentIn F x) ↔ x ∈ F
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>H1 : IsPreconnected s<VAR>H2 : x ∈ s<GOAL>s ⊆ connectedComponent x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>x : α<VAR>F : Set α<VAR>hs : IsPreconnected s<VAR>hxs : x ∈ s<VAR>hsF : s ⊆ F<GOAL>s ⊆ connectedComponentIn F x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>H1 : IsConnected s<VAR>H2 : x ∈ s<GOAL>s ⊆ connectedComponent x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>F : Set α<VAR>h : IsPreconnected F<VAR>hx : x ∈ F<GOAL>connectedComponentIn F x = F
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x y : α<VAR>h : y ∈ connectedComponent x<GOAL>connectedComponent x = connectedComponent y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x y : α<GOAL>connectedComponent x = connectedComponent y ↔ x ∈ connectedComponent y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x y : α<VAR>F : Set α<VAR>h : y ∈ connectedComponentIn F x<GOAL>connectedComponentIn F x = connectedComponentIn F y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>connectedComponentIn Set.univ x = connectedComponent x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x y : α<VAR>h : connectedComponent x ≠ connectedComponent y<GOAL>Disjoint (connectedComponent x) (connectedComponent y)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>IsClosed (connectedComponent x)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>h : Continuous f<VAR>a : α<GOAL>f '' connectedComponent a ⊆ connectedComponent (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : Continuous f<VAR>hx : a ∈ s<GOAL>f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>h : Continuous f<VAR>a : α<GOAL>Set.MapsTo f (connectedComponent a) (connectedComponent (f a))
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>h : Continuous f<VAR>a : α<VAR>hx : a ∈ s<GOAL>Set.MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a))
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>irreducibleComponent x ⊆ connectedComponent x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>F G : Set α<VAR>h : F ⊆ G<GOAL>connectedComponentIn F x ⊆ connectedComponentIn G x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>self : PreconnectedSpace α<GOAL>IsPreconnected Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>self : ConnectedSpace α<GOAL>Nonempty α
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>ConnectedSpace α<GOAL>IsConnected Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>PreconnectedSpace α ↔ IsPreconnected Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>ConnectedSpace α ↔ IsConnected Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>PreconnectedSpace α<VAR>f : α → β<VAR>h : Continuous f<GOAL>IsPreconnected (Set.range f)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ConnectedSpace α<VAR>f : α → β<VAR>h : Continuous f<GOAL>IsConnected (Set.range f)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>ConnectedSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>hf' : Continuous f<GOAL>ConnectedSpace β
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>PreconnectedSpace α<VAR>f : α → β<VAR>hf : DenseRange f<VAR>hc : Continuous f<GOAL>PreconnectedSpace β
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>ConnectedSpace α ↔ ∃ x, connectedComponent x = Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>PreconnectedSpace α ↔ ∀ (x : α), connectedComponent x = Set.univ
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>h : PreconnectedSpace X<VAR>x : X<GOAL>connectedComponent x = Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>h : IsPreconnected s<GOAL>PreconnectedSpace ↑s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>h : IsConnected s<GOAL>ConnectedSpace ↑s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>IsPreconnected s ↔ PreconnectedSpace ↑s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>IsConnected s ↔ ConnectedSpace ↑s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>x : E<GOAL>UniqueMDiffWithinAt 𝓘(𝕜, E) s x ↔ UniqueDiffWithinAt 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<GOAL>UniqueMDiffOn 𝓘(𝕜, E) s ↔ UniqueDiffOn 𝕜 s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>x : E<GOAL>writtenInExtChartAt 𝓘(𝕜, E) 𝓘(𝕜, E') x f = f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<VAR>f' : TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, E') (f x)<GOAL>HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x f' ↔ HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>x : E<VAR>f' : TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, E') (f x)<GOAL>HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f' ↔ HasFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>x : E<GOAL>MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x ↔ DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<GOAL>MDifferentiableOn 𝓘(𝕜, E) 𝓘(𝕜, E') f s ↔ DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E → E'<GOAL>MDifferentiable 𝓘(𝕜, E) 𝓘(𝕜, E') f ↔ Differentiable 𝕜 f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>x : E<GOAL>mfderiv 𝓘(𝕜, E) 𝓘(𝕜, E') f x = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>f : M → M'<VAR>f' : E →L[𝕜] E'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hd : DenseRange ⇑f'<GOAL>UniqueMDiffWithinAt I' (f '' s) (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>hs : UniqueMDiffOn I s<VAR>f : M → M'<VAR>f' : M → E →L[𝕜] E'<VAR>hf : ∀ x ∈ s, HasMFDerivWithinAt I I' f s x (f' x)<VAR>hd : ∀ x ∈ s, DenseRange ⇑(f' x)<GOAL>UniqueMDiffOn I' (f '' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>hs : UniqueMDiffOn I s<VAR>f : M → M'<VAR>hf : MDifferentiableOn I I' f s<VAR>hd : ∀ x ∈ s, DenseRange ⇑(mfderivWithin I I' f s x)<GOAL>UniqueMDiffOn I' (f '' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>e : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<VAR>hx : x ∈ e.source<GOAL>UniqueMDiffWithinAt I' (e.target ∩ ↑e.symm ⁻¹' s) (↑e x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>hs : UniqueMDiffOn I s<VAR>e : PartialHomeomorph M M'<VAR>he : PartialHomeomorph.MDifferentiable I I' e<GOAL>UniqueMDiffOn I' (e.target ∩ ↑e.symm ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>hs : UniqueMDiffOn I s<VAR>x : M<GOAL>UniqueDiffOn 𝕜 ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>s : Set M<VAR>hs : UniqueMDiffOn I s<VAR>x : M<VAR>y : M'<VAR>f : M → M'<VAR>hf : ContinuousOn f s<GOAL>UniqueDiffOn 𝕜 ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>Z : M → Type u_9<VAR>TopologicalSpace (Bundle.TotalSpace F Z)<VAR>(b : M) → TopologicalSpace (Z b)<VAR>(b : M) → AddCommMonoid (Z b)<VAR>(b : M) → Module 𝕜 (Z b)<VAR>FiberBundle F Z<VAR>VectorBundle 𝕜 F Z<VAR>SmoothVectorBundle F Z I<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<GOAL>PartialHomeomorph.MDifferentiable (I.prod 𝓘(𝕜, F)) (I.prod 𝓘(𝕜, F)) e.toPartialHomeomorph
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>Z : M → Type u_9<VAR>TopologicalSpace (Bundle.TotalSpace F Z)<VAR>(b : M) → TopologicalSpace (Z b)<VAR>(b : M) → AddCommMonoid (Z b)<VAR>(b : M) → Module 𝕜 (Z b)<VAR>FiberBundle F Z<VAR>VectorBundle 𝕜 F Z<VAR>SmoothVectorBundle F Z I<VAR>p : Bundle.TotalSpace F Z<VAR>hs : UniqueMDiffWithinAt I s p.proj<GOAL>UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (Bundle.TotalSpace.proj ⁻¹' s) p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>Z : M → Type u_9<VAR>TopologicalSpace (Bundle.TotalSpace F Z)<VAR>(b : M) → TopologicalSpace (Z b)<VAR>(b : M) → AddCommMonoid (Z b)<VAR>(b : M) → Module 𝕜 (Z b)<VAR>FiberBundle F Z<VAR>VectorBundle 𝕜 F Z<VAR>SmoothVectorBundle F Z I<VAR>b : M<VAR>hs : UniqueMDiffWithinAt I s b<VAR>x : Z b<GOAL>UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (Bundle.TotalSpace.proj ⁻¹' s) { proj := b, snd := x }
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>Z : M → Type u_9<VAR>TopologicalSpace (Bundle.TotalSpace F Z)<VAR>(b : M) → TopologicalSpace (Z b)<VAR>(b : M) → AddCommMonoid (Z b)<VAR>(b : M) → Module 𝕜 (Z b)<VAR>FiberBundle F Z<VAR>VectorBundle 𝕜 F Z<VAR>SmoothVectorBundle F Z I<VAR>hs : UniqueMDiffOn I s<GOAL>UniqueMDiffOn (I.prod 𝓘(𝕜, F)) (Bundle.TotalSpace.proj ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>hs : UniqueMDiffOn I s<GOAL>UniqueMDiffOn I.tangent (Bundle.TotalSpace.proj ⁻¹' s)
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>t : TopologicalSpace 𝕜<VAR>h₁ : TopologicalAddGroup 𝕜<VAR>h₂ : ContinuousSMul 𝕜 𝕜<VAR>h₃ : T2Space 𝕜<GOAL>t = UniformSpace.toTopologicalSpace