ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>α : Type u_8<VAR>l : Filter α<VAR>g : α → M<VAR>hg : ∀ᶠ (z : α) in l, g z ∈ f.source<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>Filter.Tendsto (↑(f.extend I) ∘ g) l (𝓝 (↑(f.extend I) y)) ↔ Filter.Tendsto g l (𝓝 y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<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>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>y : M<VAR>hy : y ∈ f.source<VAR>hgy : g y ∈ f'.source<VAR>hmaps : Set.MapsTo g s f'.source<GOAL>ContinuousWithinAt (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I) (↑(f.extend I) y) ↔ ContinuousWithinAt g s y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<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>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s : Set M<VAR>f' : PartialHomeomorph M' H'<VAR>g : M → M'<VAR>hs : s ⊆ f.source<VAR>hmaps : Set.MapsTo g s f'.source<GOAL>ContinuousOn (↑(f'.extend I') ∘ g ∘ ↑(f.extend I).symm) (↑(f.extend I) '' s) ↔ ContinuousOn g 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 t : Set M<VAR>x : M<VAR>h : x ∈ f.source<VAR>ht : t ∈ 𝓝[s] x<GOAL>↑(f.extend I).symm ⁻¹' t ∈ 𝓝[↑(f.extend I).symm ⁻¹' s ∩ 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>t : Set M<VAR>x : M<VAR>h : x ∈ f.source<VAR>ht : t ∈ 𝓝 x<GOAL>↑(f.extend I).symm ⁻¹' t ∈ 𝓝 (↑(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>s t : Set M<GOAL>↑(f.extend I).symm ⁻¹' (s ∩ t) ∩ Set.range ↑I = ↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I ∩ ↑(f.extend I).symm ⁻¹' 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>s : Set M<VAR>x : M<VAR>hx : x ∈ f.source<GOAL>↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I =ᶠ[𝓝 (↑(f.extend I) x)] (f.extend I).target ∩ ↑(f.extend I).symm ⁻¹' 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>x : M<VAR>hs : s ⊆ f.source<VAR>hx : x ∈ f.source<GOAL>↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I =ᶠ[𝓝 (↑(f.extend I) x)] ↑(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 f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>((f.extend I).symm ≫ f'.extend I).source = ↑I '' (f.symm ≫ₕ 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 f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>↑(f.extend I) '' (f.source ∩ f'.source) = ((f.extend I).symm ≫ 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 f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : E<VAR>hx : x ∈ ((f.extend I).symm ≫ f'.extend I).source<GOAL>((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[Set.range ↑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 f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x : M<VAR>hxf : x ∈ f.source<VAR>hxf' : x ∈ f'.source<GOAL>((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[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 f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>hf : f ∈ SmoothManifoldWithCorners.maximalAtlas I M<VAR>hf' : f' ∈ SmoothManifoldWithCorners.maximalAtlas I M<GOAL>ContDiffOn 𝕜 ⊤ (↑(f.extend I) ∘ ↑(f'.extend I).symm) ((f'.extend I).symm ≫ 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 f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>hf : f ∈ SmoothManifoldWithCorners.maximalAtlas I M<VAR>hf' : f' ∈ SmoothManifoldWithCorners.maximalAtlas I M<VAR>x : E<VAR>hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source<GOAL>ContDiffWithinAt 𝕜 ⊤ (↑(f.extend I) ∘ ↑(f'.extend I).symm) (Set.range ↑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 f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>hf : f ∈ SmoothManifoldWithCorners.maximalAtlas I M<VAR>hf' : f' ∈ SmoothManifoldWithCorners.maximalAtlas I M<VAR>x : M<VAR>hxf : x ∈ f.source<VAR>hxf' : x ∈ f'.source<GOAL>ContDiffWithinAt 𝕜 ⊤ (↑(f.extend I) ∘ ↑(f'.extend I).symm) (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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>↑(extChartAt I x) = ↑I ∘ ↑(chartAt H 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>↑(extChartAt I x).symm = ↑(chartAt H x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>(extChartAt I x).source = (chartAt H x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>IsOpen (extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>x ∈ (extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>↑(extChartAt I x) x ∈ (extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>(extChartAt I x).target = ↑I.symm ⁻¹' (chartAt H x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>UniqueDiffOn 𝕜 (extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>UniqueDiffWithinAt 𝕜 (extChartAt I x).target (↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>↑(extChartAt I x).symm (↑(extChartAt I x) 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>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>ChartedSpace H M<VAR>x : M<VAR>hs : s ⊆ (chartAt H x).source<GOAL>Set.MapsTo (↑(extChartAt I x)) s (↑(extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x x' : M<VAR>h : x' ∈ (extChartAt I x).source<GOAL>(extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>(extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>ChartedSpace H M<VAR>x x' : M<VAR>h : x' ∈ (extChartAt I x).source<GOAL>(extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>ChartedSpace H M<VAR>x : M<GOAL>(extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>ContinuousOn (↑(extChartAt I x)) (extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x x' : M<VAR>h : x' ∈ (extChartAt I x).source<GOAL>ContinuousAt (↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>ContinuousAt (↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x y : M<VAR>hy : y ∈ (extChartAt I x).source<GOAL>Filter.map (↑(extChartAt I x)) (𝓝 y) = 𝓝[Set.range ↑I] ↑(extChartAt I x) 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>Filter.map (↑(extChartAt I x)) (𝓝 x) = 𝓝[Set.range ↑I] ↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>I.Boundaryless<VAR>x : M<GOAL>Filter.map (↑(extChartAt I x)) (𝓝 x) = 𝓝 (↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>ChartedSpace H M<VAR>I.Boundaryless<VAR>x : M<VAR>hx : s ∈ 𝓝 x<GOAL>↑(extChartAt I x) '' s ∈ 𝓝 (↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x y : M<VAR>hy : y ∈ (extChartAt I x).source<GOAL>(extChartAt I x).target ∈ 𝓝[Set.range ↑I] ↑(extChartAt I x) 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>(extChartAt I x).target ∈ 𝓝[Set.range ↑I] ↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>I.Boundaryless<VAR>x : M<GOAL>IsOpen (extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>I.Boundaryless<VAR>x : M<GOAL>(extChartAt I x).target ∈ 𝓝 (↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>I.Boundaryless<VAR>x : M<VAR>y : E<VAR>m : y ∈ (extChartAt I x).target<GOAL>(extChartAt I x).target ∈ 𝓝 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>(extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x y : M<VAR>hy : y ∈ (extChartAt I x).source<GOAL>𝓝[(extChartAt I x).target] ↑(extChartAt I x) y = 𝓝[Set.range ↑I] ↑(extChartAt I x) 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>𝓝[(extChartAt I x).target] ↑(extChartAt I x) x = 𝓝[Set.range ↑I] ↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<VAR>y : E<VAR>h : y ∈ (extChartAt I x).target<GOAL>ContinuousAt (↑(extChartAt I x).symm) 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x x' : M<VAR>h : x' ∈ (extChartAt I x).source<GOAL>ContinuousAt (↑(extChartAt I x).symm) (↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>ContinuousAt (↑(extChartAt I x).symm) (↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>ContinuousOn (↑(extChartAt I x).symm) (extChartAt I x).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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>IsOpen ((extChartAt I x).source ∩ ↑(extChartAt I x) ⁻¹' 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>IsOpen ((chartAt H x).source ∩ ↑(extChartAt I x) ⁻¹' 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>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>ChartedSpace H M<VAR>x y : M<VAR>hy : y ∈ (extChartAt I x).source<GOAL>Filter.map (↑(extChartAt I x)) (𝓝[s] y) = 𝓝[↑(extChartAt I x) '' ((extChartAt I x).source ∩ s)] ↑(extChartAt I x) 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>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>ChartedSpace H M<VAR>x : M<GOAL>Filter.map (↑(extChartAt I x)) (𝓝[s] x) = 𝓝[↑(extChartAt I x) '' ((extChartAt I x).source ∩ s)] ↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>ChartedSpace H M<VAR>x y : M<VAR>hy : y ∈ (extChartAt I x).source<GOAL>Filter.map (↑(extChartAt I x)) (𝓝[s] y) = 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I] ↑(extChartAt I x) 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>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>ChartedSpace H M<VAR>x : M<GOAL>Filter.map (↑(extChartAt I x)) (𝓝[s] x) = 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I] ↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>ChartedSpace H M<VAR>x y : M<VAR>hy : y ∈ (extChartAt I x).source<GOAL>Filter.map (↑(extChartAt I x).symm) (𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I] ↑(extChartAt I x) 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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x y : M<VAR>hy : y ∈ (extChartAt I x).source<GOAL>Filter.map (↑(extChartAt I x).symm) (𝓝[Set.range ↑I] ↑(extChartAt I x) y) = 𝓝 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>I : ModelWithCorners 𝕜 E H<VAR>s : Set M<VAR>ChartedSpace H M<VAR>x : M<GOAL>Filter.map (↑(extChartAt I x).symm) (𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I] ↑(extChartAt I x) x) = 𝓝[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>I : ModelWithCorners 𝕜 E H<VAR>ChartedSpace H M<VAR>x : M<GOAL>Filter.map (↑(extChartAt I x).symm) (𝓝[Set.range ↑I] ↑(extChartAt I x) 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>I : ModelWithCorners 𝕜 E H<VAR>s t : Set M<VAR>ChartedSpace H M<VAR>x x' : M<VAR>h : x' ∈ (extChartAt I x).source<VAR>ht : t ∈ 𝓝[s] x'<GOAL>↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I] ↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>s t : Set M<VAR>ChartedSpace H M<VAR>x : M<VAR>ht : t ∈ 𝓝[s] x<GOAL>↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I] ↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>t : Set M<VAR>ChartedSpace H M<VAR>x x' : M<VAR>h : x' ∈ (extChartAt I x).source<VAR>ht : t ∈ 𝓝 x'<GOAL>↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝 (↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>t : Set M<VAR>ChartedSpace H M<VAR>x : M<VAR>ht : t ∈ 𝓝 x<GOAL>↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝 (↑(extChartAt 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>I : ModelWithCorners 𝕜 E H<VAR>s t : Set M<VAR>ChartedSpace H M<VAR>x : M<GOAL>↑(extChartAt I x).symm ⁻¹' (s ∩ t) ∩ Set.range ↑I = ↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>I : ModelWithCorners 𝕜 E H<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s : Set M<VAR>ChartedSpace H M<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>hc : ContinuousWithinAt f s x<GOAL>𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I] ↑(extChartAt I x) x = 𝓝[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)] ↑(extChartAt I x) x