ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>l : E →ₗ[𝕜] 𝕜<VAR>hl : IsClosed ↑(LinearMap.ker l)<GOAL>Continuous ⇑l
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>l : E →ₗ[𝕜] 𝕜<GOAL>Continuous ⇑l ↔ IsClosed ↑(LinearMap.ker l)
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>l : E →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>hs₁ : IsOpen s<VAR>hs₂ : s.Nonempty<VAR>hs₃ : ∀ x ∈ s, l x ≠ 0<GOAL>Continuous ⇑l
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>ι : Type v<VAR>Fintype ι<VAR>ξ : Basis ι 𝕜 E<GOAL>Continuous ⇑ξ.equivFun
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F' : Type x<VAR>AddCommGroup F'<VAR>Module 𝕜 F'<VAR>TopologicalSpace F'<VAR>TopologicalAddGroup F'<VAR>ContinuousSMul 𝕜 F'<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F'<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>ι : Type u_1<VAR>Finite ι<VAR>ξ : Basis ι 𝕜 E<GOAL>Continuous ⇑ξ.equivFun
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F' : Type x<VAR>AddCommGroup F'<VAR>Module 𝕜 F'<VAR>TopologicalSpace F'<VAR>TopologicalAddGroup F'<VAR>ContinuousSMul 𝕜 F'<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F'<GOAL>⇑(LinearMap.toContinuousLinearMap f) = ⇑f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F' : Type x<VAR>AddCommGroup F'<VAR>Module 𝕜 F'<VAR>TopologicalSpace F'<VAR>TopologicalAddGroup F'<VAR>ContinuousSMul 𝕜 F'<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F'<GOAL>↑(LinearMap.toContinuousLinearMap f) = f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F' : Type x<VAR>AddCommGroup F'<VAR>Module 𝕜 F'<VAR>TopologicalSpace F'<VAR>TopologicalAddGroup F'<VAR>ContinuousSMul 𝕜 F'<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<GOAL>⇑LinearMap.toContinuousLinearMap.symm = ContinuousLinearMap.toLinearMap
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] E<GOAL>(LinearMap.toContinuousLinearMap f).det = LinearMap.det f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F' : Type x<VAR>AddCommGroup F'<VAR>Module 𝕜 F'<VAR>TopologicalSpace F'<VAR>TopologicalAddGroup F'<VAR>ContinuousSMul 𝕜 F'<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F'<GOAL>LinearMap.ker (LinearMap.toContinuousLinearMap f) = LinearMap.ker f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F' : Type x<VAR>AddCommGroup F'<VAR>Module 𝕜 F'<VAR>TopologicalSpace F'<VAR>TopologicalAddGroup F'<VAR>ContinuousSMul 𝕜 F'<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F'<GOAL>LinearMap.range (LinearMap.toContinuousLinearMap f) = LinearMap.range f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : F →ₗ[𝕜] E<VAR>hf : Function.Surjective ⇑f<GOAL>IsOpenMap ⇑f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>T2Space F<VAR>FiniteDimensional 𝕜 E<VAR>e : E ≃ₗ[𝕜] F<GOAL>↑↑e.toContinuousLinearEquiv = ↑e
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>T2Space F<VAR>FiniteDimensional 𝕜 E<VAR>e : E ≃ₗ[𝕜] F<GOAL>⇑e.toContinuousLinearEquiv = ⇑e
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>T2Space F<VAR>FiniteDimensional 𝕜 E<VAR>e : E ≃ₗ[𝕜] F<GOAL>↑↑e.toContinuousLinearEquiv.symm = ↑e.symm
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>T2Space F<VAR>FiniteDimensional 𝕜 E<VAR>e : E ≃ₗ[𝕜] F<GOAL>⇑e.toContinuousLinearEquiv.symm = ⇑e.symm
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>T2Space F<VAR>FiniteDimensional 𝕜 E<VAR>e : E ≃ₗ[𝕜] F<GOAL>e.toContinuousLinearEquiv.toLinearEquiv = e
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>T2Space F<VAR>FiniteDimensional 𝕜 E<VAR>e : E ≃ₗ[𝕜] F<GOAL>e.toContinuousLinearEquiv.symm.toLinearEquiv = e.symm
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>T2Space F<VAR>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<VAR>cond : FiniteDimensional.finrank 𝕜 E = FiniteDimensional.finrank 𝕜 F<GOAL>Nonempty (E ≃L[𝕜] F)
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>T2Space F<VAR>FiniteDimensional 𝕜 E<VAR>FiniteDimensional 𝕜 F<GOAL>Nonempty (E ≃L[𝕜] F) ↔ FiniteDimensional.finrank 𝕜 E = FiniteDimensional.finrank 𝕜 F
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>Finite ι<VAR>T2Space E<VAR>v : Basis ι 𝕜 E<VAR>f : ι → F<GOAL>↑(v.constrL f) = (v.constr 𝕜) f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>Finite ι<VAR>T2Space E<VAR>v : Basis ι 𝕜 E<GOAL>∀ (a : E) (a_1 : ι), v.equivFunL a a_1 = (v.repr a) a_1
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>Finite ι<VAR>T2Space E<VAR>v : Basis ι 𝕜 E<VAR>x : E<GOAL>v.equivFunL.symm ⇑(v.repr x) = x
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>ι : Type u_2<VAR>Fintype ι<VAR>v : Basis ι 𝕜 E<VAR>f : ι → F<VAR>e : E<GOAL>(v.constrL f) e = ∑ i : ι, v.equivFun e i • f i
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>AddCommGroup F<VAR>Module 𝕜 F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul 𝕜 F<VAR>CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>Finite ι<VAR>T2Space E<VAR>v : Basis ι 𝕜 E<VAR>f : ι → F<VAR>i : ι<GOAL>(v.constrL f) (v i) = f i
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : E →L[𝕜] E<VAR>hf : f.det ≠ 0<GOAL>↑(f.toContinuousLinearEquivOfDetNeZero hf) = f
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>CompleteSpace 𝕜<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>f : E →L[𝕜] E<VAR>hf : f.det ≠ 0<VAR>x : E<GOAL>(f.toContinuousLinearEquivOfDetNeZero hf) x = f x
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>a b c d : 𝕜<GOAL>LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd 𝕜) (Basis.finTwoProd 𝕜)) !![a, b; c, d]) = (a • ContinuousLinearMap.fst 𝕜 𝕜 𝕜 + b • ContinuousLinearMap.snd 𝕜 𝕜 𝕜).prod (c • ContinuousLinearMap.fst 𝕜 𝕜 𝕜 + d • ContinuousLinearMap.snd 𝕜 𝕜 𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>AddCommGroup E<VAR>UniformSpace E<VAR>T2Space E<VAR>UniformAddGroup E<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>FiniteDimensional 𝕜 E<GOAL>CompleteSpace E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>AddCommGroup E<VAR>UniformSpace E<VAR>T2Space E<VAR>UniformAddGroup E<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>s : Submodule 𝕜 E<VAR>FiniteDimensional 𝕜 ↥s<GOAL>IsComplete ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>TopologicalAddGroup E<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>s : Submodule 𝕜 E<VAR>FiniteDimensional 𝕜 ↥s<GOAL>IsClosed ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>TopologicalAddGroup E<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>AddCommGroup F<VAR>TopologicalSpace F<VAR>T2Space F<VAR>TopologicalAddGroup F<VAR>Module 𝕜 F<VAR>ContinuousSMul 𝕜 F<VAR>FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F<VAR>hf : LinearMap.ker f = ⊥<GOAL>ClosedEmbedding ⇑f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>TopologicalAddGroup E<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>c : E<VAR>hc : c ≠ 0<GOAL>ClosedEmbedding fun x => x • c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>T2Space E<VAR>TopologicalAddGroup E<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>c : E<GOAL>IsClosedMap fun x => x • c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>Module 𝕜 E<VAR>ContinuousSMul 𝕜 E<VAR>AddCommGroup F<VAR>TopologicalSpace F<VAR>T2Space F<VAR>TopologicalAddGroup F<VAR>Module 𝕜 F<VAR>ContinuousSMul 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E →L[𝕜] F<VAR>hf : LinearMap.range f = ⊤<GOAL>∃ g, f.comp g = ContinuousLinearMap.id 𝕜 F
<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>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<GOAL>(contDiffGroupoid ⊤ I).LocalInvariantProp (contDiffGroupoid ⊤ I') (DifferentiableWithinAtProp I I')
<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>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>f : M → M'<VAR>s : Set M<VAR>x : M<GOAL>MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) 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>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>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>hf : MDifferentiableWithinAt I I' f s x<GOAL>ContinuousWithinAt f s 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>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>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>hf : MDifferentiableWithinAt I I' f s x<GOAL>DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) 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>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>f : M → M'<VAR>x : M<GOAL>MDifferentiableAt I I' f x ↔ ContinuousAt f x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (Set.range ↑I) (↑(extChartAt I x) 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>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>f : M → M'<VAR>x : M<VAR>hf : MDifferentiableAt I I' f x<GOAL>ContinuousAt 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>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>f : M → M'<VAR>x : M<VAR>hf : MDifferentiableAt I I' f x<GOAL>DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (Set.range ↑I) (↑(extChartAt I x) x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>I.Boundaryless<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>c : M<VAR>hd : ∀ᶠ (z : M) in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z<VAR>hc : IsLocalMax (norm ∘ f) c<GOAL>∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>I.Boundaryless<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>U : Set M<VAR>c : M<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<GOAL>Set.EqOn (norm ∘ f) (Function.const M ‖f c‖) U
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>I.Boundaryless<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>StrictConvexSpace ℝ F<VAR>f : M → F<VAR>U : Set M<VAR>c : M<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<GOAL>Set.EqOn f (Function.const M (f c)) U
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>I.Boundaryless<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>U : Set M<VAR>a b : M<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hpc : IsPreconnected U<VAR>hc : IsCompact U<VAR>ho : IsOpen U<VAR>ha : a ∈ U<VAR>hb : b ∈ U<GOAL>f a = f b
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>I.Boundaryless<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>CompactSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>f : M → F<VAR>hf : MDifferentiable I 𝓘(ℂ, F) f<GOAL>IsLocallyConstant f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>I.Boundaryless<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>CompactSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>PreconnectedSpace M<VAR>f : M → F<VAR>hf : MDifferentiable I 𝓘(ℂ, F) f<VAR>a b : M<GOAL>f a = f b
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>I.Boundaryless<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>CompactSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>PreconnectedSpace M<VAR>f : M → F<VAR>hf : MDifferentiable I 𝓘(ℂ, F) f<GOAL>∃ v, f = Function.const M v
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>hs : IsPreconnected s<VAR>ht : IsClopen t<VAR>hne : (s ∩ t).Nonempty<GOAL>s ⊆ t
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (π i)<VAR>s : Set ((i : ι) × π i)<GOAL>IsConnected s ↔ ∃ i t, IsConnected t ∧ s = Sigma.mk i '' t
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>hι : Nonempty ι<VAR>(i : ι) → TopologicalSpace (π i)<VAR>s : Set ((i : ι) × π i)<GOAL>IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = Sigma.mk i '' t
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set (α ⊕ β)<GOAL>IsConnected s ↔ (∃ t, IsConnected t ∧ s = Sum.inl '' t) ∨ ∃ t, IsConnected t ∧ s = Sum.inr '' t
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set (α ⊕ β)<GOAL>IsPreconnected s ↔ (∃ t, IsPreconnected t ∧ s = Sum.inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = Sum.inr '' t
<VAR>α : Type u<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>TopologicalSpace α<VAR>ConnectedSpace α<VAR>(i : ι) → TopologicalSpace (π i)<VAR>f : α → (i : ι) × π i<VAR>hf : Continuous f<GOAL>∃ i g, Continuous g ∧ f = Sigma.mk i ∘ g
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>PreconnectedSpace α<VAR>s t : Set α<GOAL>IsOpen s → IsOpen t → s ∪ t = Set.univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>PreconnectedSpace α<VAR>s : Set α<GOAL>IsClopen s ↔ s = ∅ ∨ s = Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>PreconnectedSpace α<VAR>s : Set α<VAR>h' : IsClopen s<VAR>h : s.Nonempty<GOAL>s = Set.univ
<VAR>α : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace α<VAR>PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_clopen : ∀ (i : ι), IsClopen (s i)<GOAL>Subsingleton ι
<VAR>α : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace α<VAR>PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_open : ∀ (i : ι), IsOpen (s i)<VAR>h_Union : ⋃ i, s i = Set.univ<GOAL>Subsingleton ι
<VAR>α : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace α<VAR>PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>Finite ι<VAR>h_closed : ∀ (i : ι), IsClosed (s i)<VAR>h_Union : ⋃ i, s i = Set.univ<GOAL>Subsingleton ι
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>PreconnectedSpace α<VAR>s : Set α<GOAL>frontier s = ∅ ↔ s = ∅ ∨ s = Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>PreconnectedSpace α<VAR>s : Set α<GOAL>(frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>PreconnectedSpace α<VAR>P : α → α → Prop<VAR>h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x<VAR>h' : Transitive P<VAR>x y : α<GOAL>P x y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>PreconnectedSpace α<VAR>P : α → α → Prop<VAR>h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y<VAR>h' : Transitive P<VAR>h'' : Symmetric P<VAR>x y : α<GOAL>P x y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>P : α → α → Prop<VAR>h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x<VAR>h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>P x y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>P : α → α → Prop<VAR>h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y<VAR>h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z<VAR>h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>P x y