ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>z : F<GOAL>↑e.symm (b, z) = { proj := b, snd := (Trivialization.continuousLinearEquivAt R e b hb).symm z }
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear R e<VAR>Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<GOAL>(Trivialization.continuousLinearEquivAt R e b ⋯).symm.trans (Trivialization.continuousLinearEquivAt R e' b ⋯) = Trivialization.coordChangeL R e e' b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>self : VectorBundleCore R B F ι<VAR>i : ι<VAR>x : B<GOAL>x ∈ self.baseSet i → ∀ (v : F), (self.coordChange i i x) v = v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>self : VectorBundleCore R B F ι<VAR>x : B<GOAL>x ∈ self.baseSet (self.indexAt x)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>self : VectorBundleCore R B F ι<VAR>i : ι<GOAL>IsOpen (self.baseSet i)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>self : VectorBundleCore R B F ι<VAR>i j : ι<GOAL>ContinuousOn (self.coordChange i j) (self.baseSet i ∩ self.baseSet j)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>self : VectorBundleCore R B F ι<VAR>i j k : ι<VAR>x : B<GOAL>x ∈ self.baseSet i ∩ self.baseSet j ∩ self.baseSet k → ∀ (v : F), (self.coordChange j k x) ((self.coordChange i j x) v) = (self.coordChange i k x) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<GOAL>Z.toFiberBundleCore.indexAt = Z.indexAt
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<GOAL>Z.toFiberBundleCore.coordChange = fun i j b => ⇑(Z.coordChange i j b)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<GOAL>Z.toFiberBundleCore.baseSet = Z.baseSet
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i j k : ι<VAR>x : B<GOAL>x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k → (Z.coordChange j k x).comp (Z.coordChange i j x) = Z.coordChange i k x
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i j : ι<VAR>p : B × F<GOAL>p ∈ (Z.trivChange i j).source ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b : B<VAR>i j : ι<GOAL>Z.toFiberBundleCore.coordChange i j b = ⇑(Z.coordChange i j b)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i : ι<VAR>p : Z.TotalSpace<GOAL>↑(Z.localTriv i) p = (p.proj, (Z.coordChange (Z.indexAt p.proj) i p.proj) p.snd)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i : ι<VAR>p : Z.TotalSpace<GOAL>p ∈ (Z.localTriv i).source ↔ p.proj ∈ Z.baseSet i
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i : ι<GOAL>Z.baseSet i = (Z.localTriv i).baseSet
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i : ι<VAR>p : B × F<GOAL>p ∈ (Z.localTriv i).target ↔ p.1 ∈ (Z.localTriv i).baseSet
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i : ι<VAR>p : B × F<GOAL>↑(Z.localTriv i).symm p = { proj := p.1, snd := (Z.coordChange i (Z.indexAt p.1) p.1) p.2 }
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i<VAR>v : F<GOAL>(Z.localTriv i).symm b v = (Z.coordChange i (Z.indexAt b) b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i j : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i ∩ Z.baseSet j<VAR>v : F<GOAL>(Trivialization.coordChangeL R (Z.localTriv i) (Z.localTriv j) b) v = (Z.coordChange i j b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b : B<GOAL>Z.localTriv (Z.indexAt b) = Z.localTrivAt b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b : B<VAR>a : F<GOAL>{ proj := b, snd := a } ∈ (Z.localTrivAt b).source
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>p : Z.TotalSpace<GOAL>↑(Z.localTrivAt p.proj) p = (p.proj, p.snd)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b : B<VAR>a : F<GOAL>↑(Z.localTrivAt b) { proj := b, snd := a } = (b, a)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b : B<GOAL>b ∈ (Z.localTrivAt b).baseSet
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<GOAL>Continuous Z.proj
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<GOAL>IsOpenMap Z.proj
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i<GOAL>Trivialization.continuousLinearMapAt R (Z.localTriv i) b = Z.coordChange (Z.indexAt b) i b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b₀ b : B<VAR>hb : b ∈ (trivializationAt F Z.Fiber b₀).baseSet<GOAL>Trivialization.continuousLinearMapAt R (trivializationAt F Z.Fiber b₀) b = Z.coordChange (Z.indexAt b) (Z.indexAt b₀) b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i<GOAL>Trivialization.symmL R (Z.localTriv i) b = Z.coordChange i (Z.indexAt b) b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b₀ b : B<VAR>hb : b ∈ (trivializationAt F Z.Fiber b₀).baseSet<GOAL>Trivialization.symmL R (trivializationAt F Z.Fiber b₀) b = Z.coordChange (Z.indexAt b₀) (Z.indexAt b) b
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField R<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b₀ b₁ b : B<VAR>hb : b ∈ (trivializationAt F Z.Fiber b₀).baseSet ∩ (trivializationAt F Z.Fiber b₁).baseSet<VAR>v : F<GOAL>(Trivialization.coordChangeL R (trivializationAt F Z.Fiber b₀) (trivializationAt F Z.Fiber b₁) b) v = (Z.coordChange (Z.indexAt b₀) (Z.indexAt b₁) b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>self : VectorPrebundle R F E<VAR>x : B<GOAL>x ∈ (self.pretrivializationAt x).baseSet
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>self : VectorPrebundle R F E<VAR>b : B<GOAL>Inducing (↑(self.pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>self : VectorPrebundle R F E<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<GOAL>e ∈ self.pretrivializationAtlas → Pretrivialization.IsLinear R e
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>self : VectorPrebundle R F E<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<GOAL>e ∈ self.pretrivializationAtlas → ∀ e' ∈ self.pretrivializationAtlas, ∃ f, ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧ ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' { proj := b, snd := e.symm b v }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>self : VectorPrebundle R F E<VAR>x : B<GOAL>self.pretrivializationAt x ∈ self.pretrivializationAtlas
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>e e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>he : e ∈ a.pretrivializationAtlas<VAR>he' : e' ∈ a.pretrivializationAtlas<GOAL>ContinuousOn (a.coordChange he he') (e.baseSet ∩ e'.baseSet)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>e e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>he : e ∈ a.pretrivializationAtlas<VAR>he' : e' ∈ a.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>(a.coordChange he he' b) v = (↑e' { proj := b, snd := e.symm b v }).2
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>e e' : Pretrivialization F Bundle.TotalSpace.proj<VAR>he : e ∈ a.pretrivializationAtlas<VAR>he' : e' ∈ a.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>(b, (a.coordChange he he' b) v) = ↑e' { proj := b, snd := e.symm b v }
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>e : Pretrivialization F Bundle.TotalSpace.proj<VAR>he : e ∈ a.pretrivializationAtlas<GOAL>Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>b : B<VAR>x : E b<GOAL>{ proj := b, snd := x } ∈ (a.pretrivializationAt b).source
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>b : B<GOAL>Bundle.TotalSpace.mk b ⁻¹' (a.pretrivializationAt b).source = Set.univ
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<VAR>b : B<GOAL>Continuous (Bundle.TotalSpace.mk b)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>NontriviallyNormedField R<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module R (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace R F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle R F E<GOAL>VectorBundle R F E
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>(x : B) → AddCommMonoid (E x)<VAR>NormedAddCommGroup F<VAR>TopologicalSpace B<VAR>(x : B) → TopologicalSpace (E x)<VAR>𝕜₁ : Type u_5<VAR>𝕜₂ : Type u_6<VAR>NontriviallyNormedField 𝕜₁<VAR>NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>B' : Type u_7<VAR>TopologicalSpace B'<VAR>NormedSpace 𝕜₁ F<VAR>(x : B) → Module 𝕜₁ (E x)<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>F' : Type u_8<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜₂ F'<VAR>E' : B' → Type u_9<VAR>(x : B') → AddCommMonoid (E' x)<VAR>(x : B') → Module 𝕜₂ (E' x)<VAR>TopologicalSpace (Bundle.TotalSpace F' E')<VAR>FiberBundle F E<VAR>VectorBundle 𝕜₁ F E<VAR>(x : B') → TopologicalSpace (E' x)<VAR>FiberBundle F' E'<VAR>VectorBundle 𝕜₂ F' E'<VAR>x₀ x : B<VAR>y₀ y : B'<VAR>ϕ : E x →SL[σ] E' y<VAR>hx : x ∈ (trivializationAt F E x₀).baseSet<VAR>hy : y ∈ (trivializationAt F' E' y₀).baseSet<GOAL>ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ = (↑(Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy)).comp (ϕ.comp ↑(Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>TopologicalSpace B<VAR>𝕜₁ : Type u_5<VAR>𝕜₂ : Type u_6<VAR>NontriviallyNormedField 𝕜₁<VAR>NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>B' : Type u_7<VAR>TopologicalSpace B'<VAR>NormedSpace 𝕜₁ F<VAR>F' : Type u_8<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜₂ F'<VAR>ι : Type u_10<VAR>ι' : Type u_11<VAR>Z : VectorBundleCore 𝕜₁ B F ι<VAR>Z' : VectorBundleCore 𝕜₂ B' F' ι'<VAR>x₀ x : B<VAR>y₀ y : B'<VAR>ϕ : F →SL[σ] F'<VAR>hx : x ∈ Z.baseSet (Z.indexAt x₀)<VAR>hy : y ∈ Z'.baseSet (Z'.indexAt y₀)<GOAL>ContinuousLinearMap.inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ = (Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y).comp (ϕ.comp (Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x))
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>s : Set X<GOAL>dimH s = ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : ↑d < dimH s<GOAL>μH[↑d] s = ⊤
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0∞<VAR>H : ∀ (d' : ℝ≥0), μH[↑d'] s = ⊤ → ↑d' ≤ d<GOAL>dimH s ≤ d
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : μH[↑d] s ≠ ⊤<GOAL>dimH s ≤ ↑d
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : μH[↑d] s = ⊤<GOAL>↑d ≤ dimH s
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : dimH s < ↑d<GOAL>μH[↑d] s = 0
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>μ : MeasureTheory.Measure X<VAR>d : ℝ≥0<VAR>h : μ ≪ μH[↑d]<VAR>s : Set X<VAR>hd : dimH s < ↑d<GOAL>μ s = 0
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : μH[↑d] s ≠ 0<GOAL>↑d ≤ dimH s
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>MeasurableSpace X<VAR>BorelSpace X<VAR>d : ℝ≥0<VAR>s : Set X<VAR>h : μH[↑d] s ≠ 0<VAR>h' : μH[↑d] s ≠ ⊤<GOAL>dimH s = ↑d
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>s t : Set X<VAR>h : s ⊆ t<GOAL>dimH s ≤ dimH t
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>s : Set X<VAR>h : s.Subsingleton<GOAL>dimH s = 0
<VAR>X : Type u_2<VAR>EMetricSpace X<GOAL>dimH ∅ = 0
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>x : X<GOAL>dimH {x} = 0
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>ι : Sort u_4<VAR>Countable ι<VAR>s : ι → Set X<GOAL>dimH (⋃ i, s i) = ⨆ i, dimH (s i)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>s : Set ι<VAR>hs : s.Countable<VAR>t : ι → Set X<GOAL>dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>S : Set (Set X)<VAR>hS : S.Countable<GOAL>dimH (⋃₀ S) = ⨆ s ∈ S, dimH s
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>s t : Set X<GOAL>dimH (s ∪ t) = max (dimH s) (dimH t)
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>s : Set X<VAR>hs : s.Countable<GOAL>dimH s = 0
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>s : Set X<VAR>hs : s.Finite<GOAL>dimH s = 0
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>s : Finset X<GOAL>dimH ↑s = 0
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>SecondCountableTopology X<VAR>s : Set X<VAR>r : ℝ≥0∞<VAR>h : r < dimH s<GOAL>∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>SecondCountableTopology X<VAR>s : Set X<GOAL>⨆ x ∈ s, Filter.limsup dimH (𝓝[s] x).smallSets = dimH s
<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>SecondCountableTopology X<VAR>s : Set X<GOAL>⨆ x, Filter.limsup dimH (𝓝[s] x).smallSets = dimH s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<GOAL>dimH (f '' s) ≤ dimH s / ↑r
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>h : HolderWith C r f<VAR>hr : 0 < r<VAR>s : Set X<GOAL>dimH (f '' s) ≤ dimH s / ↑r
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>h : HolderWith C r f<VAR>hr : 0 < r<GOAL>dimH (Set.range f) ≤ dimH Set.univ / ↑r
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>s : Set X<VAR>hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, HolderOnWith C r f t<GOAL>dimH (f '' s) ≤ dimH s / ↑r
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s<GOAL>dimH (Set.range f) ≤ dimH Set.univ / ↑r
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>K : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>h : LipschitzOnWith K f s<GOAL>dimH (f '' s) ≤ dimH s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>K : ℝ≥0<VAR>f : X → Y<VAR>h : LipschitzWith K f<VAR>s : Set X<GOAL>dimH (f '' s) ≤ dimH s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>K : ℝ≥0<VAR>f : X → Y<VAR>h : LipschitzWith K f<GOAL>dimH (Set.range f) ≤ dimH Set.univ
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>SecondCountableTopology X<VAR>f : X → Y<VAR>s : Set X<VAR>hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t<GOAL>dimH (f '' s) ≤ dimH s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>SecondCountableTopology X<VAR>f : X → Y<VAR>hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s<GOAL>dimH (Set.range f) ≤ dimH Set.univ
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>K : ℝ≥0<VAR>f : X → Y<VAR>hf : AntilipschitzWith K f<VAR>s : Set Y<GOAL>dimH (f ⁻¹' s) ≤ dimH s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>K : ℝ≥0<VAR>f : X → Y<VAR>hf : AntilipschitzWith K f<VAR>s : Set X<GOAL>dimH s ≤ dimH (f '' s)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>f : X → Y<VAR>hf : Isometry f<VAR>s : Set X<GOAL>dimH (f '' s) = dimH s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>e : X ≃ᵢ Y<VAR>s : Set X<GOAL>dimH (⇑e '' s) = dimH s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>e : X ≃ᵢ Y<VAR>s : Set Y<GOAL>dimH (⇑e ⁻¹' s) = dimH s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>EMetricSpace X<VAR>EMetricSpace Y<VAR>e : X ≃ᵢ Y<GOAL>dimH Set.univ = dimH Set.univ
<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>e : E ≃L[𝕜] F<VAR>s : Set E<GOAL>dimH (⇑e '' s) = dimH s
<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>e : E ≃L[𝕜] F<VAR>s : Set F<GOAL>dimH (⇑e ⁻¹' s) = dimH s
<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>e : E ≃L[𝕜] F<GOAL>dimH Set.univ = dimH Set.univ
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>x : ι → ℝ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>dimH (Metric.ball x r) = ↑(Fintype.card ι)
<VAR>n : ℕ<VAR>x : Fin n → ℝ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>dimH (Metric.ball x r) = ↑n
<VAR>ι : Type u_5<VAR>Fintype ι<GOAL>dimH Set.univ = ↑(Fintype.card ι)
<VAR>n : ℕ<GOAL>dimH Set.univ = ↑n