ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<GOAL>↑I.symm ∘ ↑I = id
<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<GOAL>Set.RightInvOn (↑I.symm) (↑I) (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>x : E<VAR>hx : x ∈ Set.range ↑I<GOAL>↑I (↑I.symm 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>s : Set H<GOAL>↑I ⁻¹' (↑I '' s) = 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>s : Set H<GOAL>↑I '' s = ↑I.symm ⁻¹' s ∩ 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<GOAL>ClosedEmbedding ↑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<GOAL>IsClosed (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>x : H<GOAL>Filter.map (↑I) (𝓝 x) = 𝓝[Set.range ↑I] ↑I 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>s : Set H<VAR>x : H<GOAL>Filter.map (↑I) (𝓝[s] x) = 𝓝[↑I '' s] ↑I 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>x : H<VAR>s : Set H<VAR>hs : s ∈ 𝓝 x<GOAL>↑I '' s ∈ 𝓝[Set.range ↑I] ↑I 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>x : H<VAR>s : Set H<GOAL>Filter.map (↑I.symm) (𝓝[↑I '' s] ↑I x) = 𝓝[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>x : H<GOAL>Filter.map (↑I.symm) (𝓝[Set.range ↑I] ↑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>s : Set H<VAR>hs : IsOpen s<GOAL>UniqueDiffOn 𝕜 (↑I.symm ⁻¹' s ∩ 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>β : Type u_4<VAR>TopologicalSpace β<VAR>e : PartialHomeomorph H β<GOAL>UniqueDiffOn 𝕜 (↑I.symm ⁻¹' e.source ∩ 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>x : H<GOAL>UniqueDiffWithinAt 𝕜 (Set.range ↑I) (↑I 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>X : Type u_4<VAR>TopologicalSpace X<VAR>f : H → X<VAR>s : Set H<VAR>x : H<GOAL>ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x) ↔ 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>LocallyCompactSpace E<VAR>I : ModelWithCorners 𝕜 E H<GOAL>LocallyCompactSpace H
<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>SecondCountableTopology E<VAR>I : ModelWithCorners 𝕜 E H<GOAL>SecondCountableTopology H
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>𝓘(𝕜, E).toPartialEquiv = PartialEquiv.refl E
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>↑𝓘(𝕜, E) = id
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<GOAL>↑𝓘(𝕜, E).symm = id
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type w<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>E' : Type v'<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type w'<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<GOAL>(I.prod I').target = (I.prod I'.toPartialEquiv).target
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type w<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>E' : Type v'<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type w'<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<GOAL>(I.prod I').source = {x | x.1 ∈ I.source ∧ x.2 ∈ I'.source}
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type w<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>E' : Type v'<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type w'<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>x : ModelProd H H'<GOAL>↑(I.prod I') x = (↑I x.1, ↑I' x.2)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type w<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>E' : Type v'<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type w'<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>x : E × E'<GOAL>↑(I.prod I').symm x = (↑I.symm x.1, ↑I'.symm x.2)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_6<VAR>TopologicalSpace H<VAR>G : Type u_8<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<GOAL>(I.prod J).toPartialEquiv = I.prod J.toPartialEquiv
<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>H : Type u_6<VAR>TopologicalSpace H<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<GOAL>↑(I.prod I') = Prod.map ↑I ↑I'
<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>H : Type u_6<VAR>TopologicalSpace H<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<GOAL>↑(I.prod I').symm = Prod.map ↑I.symm ↑I'.symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<GOAL>𝓘(𝕜, E × F) = 𝓘(𝕜, E).prod 𝓘(𝕜, F)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_6<VAR>TopologicalSpace H<VAR>G : Type u_8<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<GOAL>Set.range ↑(I.prod J) = Set.range ↑I ×ˢ Set.range ↑J
<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>self : I.Boundaryless<GOAL>Set.range ↑I = 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>I.Boundaryless<GOAL>Set.range ↑I = 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>I.Boundaryless<GOAL>∀ (a : E), I.toHomeomorph.symm a = ↑I.symm a
<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>I.Boundaryless<GOAL>∀ (a : H), I.toHomeomorph a = ↑I a
<VAR>m 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>h : m ≤ n<GOAL>contDiffGroupoid n I ≤ contDiffGroupoid m 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<GOAL>contDiffGroupoid 0 I = continuousGroupoid H
<VAR>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>s : Set H<VAR>hs : IsOpen s<GOAL>PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I
<VAR>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>e : PartialHomeomorph M H<GOAL>e.symm ≫ₕ e ∈ contDiffGroupoid n 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>E' : Type u_5<VAR>H' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>e : PartialHomeomorph H H<VAR>e' : PartialHomeomorph H' H'<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>he' : e' ∈ contDiffGroupoid ⊤ I'<GOAL>e.prod e' ∈ contDiffGroupoid ⊤ (I.prod 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>gr : HasGroupoid M (contDiffGroupoid ⊤ I)<GOAL>SmoothManifoldWithCorners I 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>h : ∀ (e e' : PartialHomeomorph M H), e ∈ atlas H M → e' ∈ atlas H M → ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(e.symm ≫ₕ e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ Set.range ↑I)<GOAL>SmoothManifoldWithCorners I 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>SmoothManifoldWithCorners I M<GOAL>atlas H M ⊆ SmoothManifoldWithCorners.maximalAtlas I 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>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>chartAt H x ∈ SmoothManifoldWithCorners.maximalAtlas I 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 e' : PartialHomeomorph M H<VAR>he : e ∈ SmoothManifoldWithCorners.maximalAtlas I M<VAR>he' : e' ∈ SmoothManifoldWithCorners.maximalAtlas I M<GOAL>e.symm ≫ₕ e' ∈ contDiffGroupoid ⊤ 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>e : PartialHomeomorph M H<VAR>h : e.source = Set.univ<GOAL>SmoothManifoldWithCorners I 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>Nonempty M<VAR>f : M → H<VAR>h : OpenEmbedding f<GOAL>SmoothManifoldWithCorners I M
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>↑(f.extend I) = ↑I ∘ ↑f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>↑(f.extend I).symm = ↑f.symm ∘ ↑I.symm
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>(f.extend I).source = f.source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>IsOpen (f.extend I).source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>(f.extend I).target = ↑I.symm ⁻¹' f.target ∩ Set.range ↑I
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>(f.extend I).target = ↑I '' f.target
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>I.Boundaryless<GOAL>IsOpen (f.extend I).target
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>hs : s ⊆ f.source<GOAL>Set.MapsTo (↑(f.extend I)) s (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : M<VAR>hxf : x ∈ f.source<GOAL>↑(f.extend I).symm (↑(f.extend I) x) = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>t : Set M<VAR>ht : t ⊆ f.source<GOAL>↑(f.extend I).symm ∘ ↑(f.extend I) '' t = t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : M<VAR>h : x ∈ f.source<GOAL>(f.extend I).source ∈ 𝓝 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>x : M<VAR>h : x ∈ f.source<GOAL>(f.extend I).source ∈ 𝓝[s] x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>ContinuousOn (↑(f.extend I)) (f.extend I).source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : M<VAR>h : x ∈ f.source<GOAL>ContinuousAt (↑(f.extend I)) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : M<VAR>hy : x ∈ f.source<GOAL>Filter.map (↑(f.extend I)) (𝓝 x) = 𝓝[Set.range ↑I] ↑(f.extend I) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>I.Boundaryless<VAR>x : M<VAR>hx : x ∈ f.source<GOAL>Filter.map (↑(f.extend I)) (𝓝 x) = 𝓝 (↑(f.extend I) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>(f.extend I).target ∈ 𝓝[Set.range ↑I] ↑(f.extend I) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>I.Boundaryless<VAR>x : M<VAR>hx : x ∈ f.source<VAR>s : Set M<VAR>h : s ∈ 𝓝 x<GOAL>↑(f.extend I) '' s ∈ 𝓝 (↑(f.extend I) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>(f.extend I).target ⊆ Set.range ↑I
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>interior (f.extend I).target ⊆ interior (Set.range ↑I)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>y : H<VAR>hy : y ∈ f.target<VAR>hy' : ↑I y ∈ interior (Set.range ↑I)<GOAL>↑I y ∈ interior (f.extend I).target
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>𝓝[(f.extend I).target] ↑(f.extend I) y = 𝓝[Set.range ↑I] ↑(f.extend I) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : E<VAR>h : x ∈ (f.extend I).target<GOAL>ContinuousAt (↑(f.extend I).symm) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : M<VAR>h : x ∈ f.source<GOAL>ContinuousAt (↑(f.extend I).symm) (↑(f.extend I) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>ContinuousOn (↑(f.extend I).symm) (f.extend I).target
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>X : Type u_8<VAR>TopologicalSpace X<VAR>g : M → X<VAR>s : Set M<VAR>x : M<GOAL>ContinuousWithinAt (g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I) (↑(f.extend I) x) ↔ ContinuousWithinAt (g ∘ ↑f.symm) (↑f.symm ⁻¹' s) (↑f x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>IsOpen ((f.extend I).source ∩ ↑(f.extend I) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>IsOpen (f.source ∩ ↑(f.extend I) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>Filter.map (↑(f.extend I)) (𝓝[s] y) = 𝓝[↑(f.extend I) '' ((f.extend I).source ∩ s)] ↑(f.extend I) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>y : M<VAR>hy : y ∈ f.source<VAR>hs : s ⊆ f.source<GOAL>Filter.map (↑(f.extend I)) (𝓝[s] y) = 𝓝[↑(f.extend I) '' s] ↑(f.extend I) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>Filter.map (↑(f.extend I)) (𝓝[s] y) = 𝓝[↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I] ↑(f.extend I) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>Filter.map (↑(f.extend I).symm) (𝓝[↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I] ↑(f.extend I) y) = 𝓝[s] y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>f : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>Filter.map (↑(f.extend I).symm) (𝓝[Set.range ↑I] ↑(f.extend I) y) = 𝓝 y