ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>TopologicalSpace X<VAR>AddGroup X<VAR>TopologicalAddGroup X<VAR>UniformSpace Y<VAR>AddCommGroup Y<VAR>UniformAddGroup Y<VAR>T0Space Y<VAR>CompactSpace Y<VAR>LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x + x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 0).HasBasis (fun x => True) V<GOAL>LocallyCompactSpace (ContinuousAddMonoidHom X Y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ⊆ coborder s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>coborder s ∩ closure s = s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>closure s ∩ coborder s = s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>coborder s = s ∪ (frontier s)ᶜ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>coborder s = Set.univ ↔ IsClosed s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>coborder s = (frontier s)ᶜ ↔ IsOpen s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsOpenMap f<VAR>s : Set Y<GOAL>coborder (f ⁻¹' s) ⊆ f ⁻¹' coborder s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>s : Set Y<GOAL>f ⁻¹' coborder s ⊆ coborder (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsOpenMap f<VAR>hf' : Continuous f<VAR>s : Set Y<GOAL>coborder (f ⁻¹' s) = f ⁻¹' coborder s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : OpenEmbedding f<VAR>s : Set Y<GOAL>coborder (f ⁻¹' s) = f ⁻¹' coborder s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsClosed (coborder s ↓∩ s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>IsLocallyClosed s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsLocallyClosed s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsLocallyClosed s<VAR>ht : IsLocallyClosed t<GOAL>IsLocallyClosed (s ∩ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set Y<VAR>hs : IsLocallyClosed s<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsLocallyClosed (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ f ⁻¹' s' = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf : Embedding f<GOAL>IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ s' ∩ Set.range f = f '' s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>hs : IsLocallyClosed s<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hf' : IsLocallyClosed (Set.range f)<GOAL>IsLocallyClosed (f '' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>[IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s), ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (closure s ↓∩ s)].TFAE
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsLocallyClosed s ↔ IsOpen (coborder s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsLocallyClosed s<GOAL>IsOpen (closure s ↓∩ s)
<VAR>α : Type u<GOAL>TopologicalSpace.IsTopologicalBasis (ultrafilterBasis α)
<VAR>α : Type u<VAR>s : Set α<GOAL>IsOpen {u | s ∈ u}
<VAR>α : Type u<VAR>b : Ultrafilter α<GOAL>Filter.Tendsto pure (↑b) (𝓝 b)
<VAR>α : Type u<VAR>b : Ultrafilter α<GOAL>Filter.comap pure (𝓝 b) ≤ ↑b
<VAR>α : Type u<GOAL>TopologicalSpace.induced pure Ultrafilter.topologicalSpace = ⊥
<VAR>α : Type u<VAR>γ : Type u_1<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>f : α → γ<GOAL>Ultrafilter.extend f ∘ pure = f
<VAR>α : Type u<VAR>γ : Type u_1<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>CompactSpace γ<VAR>f : α → γ<GOAL>Continuous (Ultrafilter.extend f)
<VAR>α : Type u<VAR>γ : Type u_1<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>CompactSpace γ<VAR>f : α → γ<VAR>b : Ultrafilter α<VAR>c : γ<GOAL>Ultrafilter.extend f b = c ↔ ↑(Ultrafilter.map f b) ≤ 𝓝 c
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>Continuous preStoneCechUnit
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>DenseRange preStoneCechUnit
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type v<VAR>TopologicalSpace β<VAR>T2Space β<VAR>CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>F G : Ultrafilter α<VAR>x : α<VAR>hF : ↑F ≤ 𝓝 x<VAR>hG : ↑G ≤ 𝓝 x<GOAL>Ultrafilter.extend g F = Ultrafilter.extend g G
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type v<VAR>TopologicalSpace β<VAR>T2Space β<VAR>CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<GOAL>preStoneCechExtend hg ∘ preStoneCechUnit = g
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type v<VAR>TopologicalSpace β<VAR>T2Space β<VAR>CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>a b : α<VAR>h : preStoneCechUnit a = preStoneCechUnit b<GOAL>g a = g b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type v<VAR>TopologicalSpace β<VAR>T2Space β<VAR>CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<GOAL>Continuous (preStoneCechExtend hg)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type v<VAR>TopologicalSpace β<VAR>T2Space β<VAR>g₁ g₂ : PreStoneCech α → β<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit<GOAL>g₁ = g₂
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>Continuous stoneCechUnit
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>DenseRange stoneCechUnit
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type v<VAR>TopologicalSpace β<VAR>T2Space β<VAR>CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<GOAL>stoneCechExtend hg ∘ stoneCechUnit = g
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type v<VAR>TopologicalSpace β<VAR>T2Space β<VAR>CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<GOAL>Continuous (stoneCechExtend hg)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type v<VAR>TopologicalSpace β<VAR>T2Space β<VAR>CompactSpace β<VAR>a b : α<VAR>f : α → β<VAR>hcf : Continuous f<VAR>h : stoneCechUnit a = stoneCechUnit b<GOAL>f a = f b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type v<VAR>TopologicalSpace β<VAR>T2Space β<VAR>g₁ g₂ : StoneCech α → β<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit<GOAL>g₁ = g₂
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>self : PartialDiffeomorph I J M N n<GOAL>ContMDiffOn J I n self.invFun self.target
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>self : PartialDiffeomorph I J M N n<GOAL>IsOpen self.target
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>self : PartialDiffeomorph I J M N n<GOAL>ContMDiffOn I J n (↑self.toPartialEquiv) self.source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>self : PartialDiffeomorph I J M N n<GOAL>IsOpen self.source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>Φ : PartialDiffeomorph I J M N n<GOAL>ContMDiffOn I J n (↑Φ.toPartialEquiv) Φ.source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>Φ : PartialDiffeomorph I J M N n<VAR>hn : 1 ≤ n<GOAL>MDifferentiableOn I J (↑Φ.toPartialEquiv) Φ.source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>Φ : PartialDiffeomorph I J M N n<VAR>hn : 1 ≤ n<VAR>x : M<VAR>hx : x ∈ Φ.source<GOAL>MDifferentiableAt I J (↑Φ.toPartialEquiv) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s : Set M<GOAL>IsLocalDiffeomorphOn I J n f s ↔ ∀ (x : ↑s), IsLocalDiffeomorphAt I J n f ↑x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<GOAL>IsLocalDiffeomorph I J n f ↔ ∀ (x : M), IsLocalDiffeomorphAt I J n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<GOAL>IsLocalDiffeomorph I J n f ↔ IsLocalDiffeomorphOn I J n f Set.univ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>hf : IsLocalDiffeomorph I J n f<VAR>s : Set M<GOAL>IsLocalDiffeomorphOn I J n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>x : M<VAR>hf : IsLocalDiffeomorphAt I J n f x<GOAL>ContMDiffAt I J n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>x : M<VAR>hf : IsLocalDiffeomorphAt I J n f x<VAR>hn : 1 ≤ n<GOAL>MDifferentiableAt I J f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s : Set M<VAR>hf : IsLocalDiffeomorphOn I J n f s<GOAL>ContMDiffOn I J n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s : Set M<VAR>hf : IsLocalDiffeomorphOn I J n f s<VAR>hn : 1 ≤ n<GOAL>MDifferentiableOn I J f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>hf : IsLocalDiffeomorph I J n f<GOAL>ContMDiff I J n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>hf : IsLocalDiffeomorph I J n f<VAR>hn : 1 ≤ n<GOAL>MDifferentiable I J f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>Φ : M ≃ₘ^n⟮I, J⟯ N<GOAL>IsLocalDiffeomorph I J n ⇑Φ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s : Set M<VAR>hf : IsLocalDiffeomorphOn I J n f s<GOAL>IsLocalHomeomorphOn f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>hf : IsLocalDiffeomorph I J n f<GOAL>IsLocalHomeomorph f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>hf : IsLocalDiffeomorph I J n f<GOAL>IsOpenMap f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>hf : IsLocalDiffeomorph I J n f<GOAL>IsOpen (Set.range f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>G : Type u_5<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>hf : IsLocalDiffeomorph I J n f<GOAL>hf.image.carrier = Set.range 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<GOAL>I.IsInteriorPoint x ↔ ↑(extChartAt I x) x ∈ interior (extChartAt I x).target
<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>x : M<GOAL>I.IsBoundaryPoint x ↔ ↑(extChartAt I x) x ∈ frontier (Set.range ↑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>x : M<GOAL>I.IsInteriorPoint x ∨ I.IsBoundaryPoint 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<GOAL>I.interior M ∪ I.boundary M = Set.univ
<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<GOAL>Disjoint (I.interior M) (I.boundary M)
<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<GOAL>I.boundary M = (I.interior M)ᶜ
<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>x : M<VAR>h : I.IsInteriorPoint x<GOAL>Set.range ↑I ∈ 𝓝 (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_7<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>self : BoundarylessManifold I M<VAR>x : M<GOAL>I.IsInteriorPoint 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>BoundarylessManifold I M<VAR>x : M<GOAL>I.IsInteriorPoint 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>BoundarylessManifold I M<GOAL>I.interior M = Set.univ
<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>BoundarylessManifold I M<GOAL>I.boundary M = ∅
<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>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<GOAL>(I.prod J).interior (M × N) = I.interior M ×ˢ J.interior N
<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>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<GOAL>(I.prod J).boundary (M × N) = Set.univ.prod (J.boundary N) ∪ (I.boundary M).prod Set.univ
<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>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>I.Boundaryless<GOAL>(I.prod J).boundary (M × N) = Set.univ.prod (J.boundary N)
<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>N : Type u_7<VAR>TopologicalSpace N<VAR>ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>J.Boundaryless<GOAL>(I.prod J).boundary (M × N) = (I.boundary M).prod Set.univ
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>a b : Rˣ<GOAL>↑(chartAt R a) b = ↑b
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>a : Rˣ<GOAL>(chartAt R a).source = Set.univ