ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>IsPreconnected s ↔ ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>IsConnected s ↔ ∀ (U : Finset (Set α)), (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>hs : IsPreconnected s<VAR>ht : IsClopen t<GOAL>Disjoint s t ∨ s ⊆ t
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>x : α<VAR>hs : IsClopen s<VAR>hx : x ∈ s<GOAL>connectedComponent x ⊆ s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>connectedComponent x ⊆ ⋂ Z, ↑Z
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Z : Set α<VAR>h : IsClopen Z<GOAL>⋃ x ∈ Z, connectedComponent x = Z
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})<VAR>hcl : ∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)<VAR>t : β<GOAL>IsConnected (f ⁻¹' connectedComponent t)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : QuotientMap f<VAR>h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})<VAR>a : α<GOAL>f ⁻¹' connectedComponent (f a) = connectedComponent a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : QuotientMap f<VAR>h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})<VAR>a : α<GOAL>f '' connectedComponent a = connectedComponent (f a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x y : α<GOAL>ConnectedComponents.mk x = ConnectedComponents.mk y ↔ connectedComponent x = connectedComponent y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x y : α<GOAL>ConnectedComponents.mk x ≠ ConnectedComponents.mk y ↔ connectedComponent x ≠ connectedComponent y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x y : α<GOAL>ConnectedComponents.mk x = ConnectedComponents.mk y ↔ x ∈ connectedComponent y
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>Function.Surjective ConnectedComponents.mk
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>QuotientMap ConnectedComponents.mk
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>Continuous ConnectedComponents.mk
<VAR>α : Type u<VAR>TopologicalSpace α<GOAL>Set.range ConnectedComponents.mk = Set.univ
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<GOAL>ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} = connectedComponent x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>U : Set α<GOAL>ConnectedComponents.mk ⁻¹' (ConnectedComponents.mk '' U) = ⋃ x ∈ U, connectedComponent x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y<GOAL>IsPreconnected s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>hs : ∀ (f : α → Bool), Continuous f → ∀ (x y : α), f x = f y<GOAL>PreconnectedSpace α
<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_4<VAR>TopologicalSpace H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>f : C^n⟮I, M; I', M'⟯<GOAL>ContMDiff I I' n ⇑f
<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_4<VAR>TopologicalSpace H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : C^⊤⟮I, M; I', M'⟯<GOAL>Smooth I I' ⇑f
<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_4<VAR>TopologicalSpace H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>f : M → M'<VAR>hf : ContMDiff I I' n f<GOAL>⇑⟨f, hf⟩ = f
<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_4<VAR>TopologicalSpace H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>f g : C^n⟮I, M; I', M'⟯<VAR>h : ⇑f = ⇑g<GOAL>f = g
<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_4<VAR>TopologicalSpace H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>f g : C^n⟮I, M; I', M'⟯<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<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_4<VAR>TopologicalSpace H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>n : ℕ∞<VAR>f : C^n⟮I', M'; I'', M''⟯<VAR>g : C^n⟮I, M; I', M'⟯<VAR>x : M<GOAL>(f.comp g) x = f (g x)
<VAR>n : ℕ<VAR>x y : EuclideanQuadrant n<VAR>h : ↑x = ↑y<GOAL>x = y
<VAR>n : ℕ<VAR>Zero (Fin n)<VAR>x y : EuclideanHalfSpace n<VAR>h : ↑x = ↑y<GOAL>x = y
<VAR>n : ℕ<VAR>Zero (Fin n)<GOAL>(Set.range fun x => ↑x) = {y | 0 ≤ y 0}
<VAR>n : ℕ<GOAL>(Set.range fun x => ↑x) = {y | ∀ (i : Fin n), 0 ≤ y i}
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<GOAL>⇑f.embeddingPiTangent = fun x i => (↑(f.toFun i) x • ↑(extChartAt I (f.c i)) x, ↑(f.toFun i) x)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<GOAL>Set.InjOn (⇑f.embeddingPiTangent) s
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>hi : Fintype ι<VAR>f : SmoothBumpCovering ι I M<GOAL>Function.Injective ⇑f.embeddingPiTangent
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>((ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))).comp (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) = mfderiv I I (↑(chartAt H (f.c (f.ind x hx)))) x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) = ⊥
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>Function.Injective ⇑(mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>Finite ι<VAR>f : SmoothBumpCovering ι I M<GOAL>∃ n e, Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧ Function.Injective e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>CompactSpace M<GOAL>∃ n e, Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧ ClosedEmbedding e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>self : PartialHomeomorph X Y<GOAL>ContinuousOn (↑self.toPartialEquiv) self.source
<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>self : PartialHomeomorph X Y<GOAL>ContinuousOn self.invFun self.target
<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>self : PartialHomeomorph X Y<GOAL>IsOpen self.source
<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>self : PartialHomeomorph X Y<GOAL>IsOpen self.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>ContinuousOn (↑e) e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>ContinuousOn (↑e.symm) e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialEquiv X Y<VAR>a : IsOpen e.source<VAR>b : IsOpen e.target<VAR>c : ContinuousOn (↑e) e.source<VAR>d : ContinuousOn e.invFun e.target<GOAL>↑{ toPartialEquiv := e, open_source := a, open_target := b, continuousOn_toFun := c, continuousOn_invFun := d } = ↑e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialEquiv X Y<VAR>a : IsOpen e.source<VAR>b : IsOpen e.target<VAR>c : ContinuousOn (↑e) e.source<VAR>d : ContinuousOn e.invFun e.target<GOAL>↑{ toPartialEquiv := e, open_source := a, open_target := b, continuousOn_toFun := c, continuousOn_invFun := d }.symm = ↑e.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Function.Injective PartialHomeomorph.toPartialEquiv
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>↑e.toPartialEquiv = ↑e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>e.invFun = ↑e.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>↑e.symm = ↑e.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>h : x ∈ e.source<GOAL>↑e x ∈ e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>↑e '' e.source ⊆ e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : Y<VAR>h : x ∈ e.target<GOAL>↑e.symm x ∈ e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>h : x ∈ e.source<GOAL>↑e.symm (↑e x) = x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : Y<VAR>h : x ∈ e.target<GOAL>↑e (↑e.symm x) = x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>y : Y<VAR>hx : x ∈ e.source<VAR>hy : y ∈ e.target<GOAL>x = ↑e.symm y ↔ ↑e x = y
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>Set.MapsTo (↑e) e.source e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>Set.MapsTo (↑e.symm) e.target e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>Set.LeftInvOn (↑e.symm) (↑e) e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>Set.RightInvOn (↑e.symm) (↑e) e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>Set.InvOn (↑e.symm) (↑e) e.source e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>Set.InjOn (↑e) e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>Set.BijOn (↑e) e.source e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>Set.SurjOn (↑e) e.source e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>s : Set X<VAR>hs : IsOpen s<VAR>t : Set Y<VAR>h : ⇑e '' s = t<GOAL>(e.toPartialHomeomorphOfImageEq s hs t h).source = s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>s : Set X<VAR>hs : IsOpen s<VAR>t : Set Y<VAR>h : ⇑e '' s = t<GOAL>(e.toPartialHomeomorphOfImageEq s hs t h).toPartialEquiv = e.toPartialEquivOfImageEq s t h
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>s : Set X<VAR>hs : IsOpen s<VAR>t : Set Y<VAR>h : ⇑e '' s = t<GOAL>↑(e.toPartialHomeomorphOfImageEq s hs t h).symm = ⇑e.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>s : Set X<VAR>hs : IsOpen s<VAR>t : Set Y<VAR>h : ⇑e '' s = t<GOAL>↑(e.toPartialHomeomorphOfImageEq s hs t h) = ⇑e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>s : Set X<VAR>hs : IsOpen s<VAR>t : Set Y<VAR>h : ⇑e '' s = t<GOAL>(e.toPartialHomeomorphOfImageEq s hs t h).target = t
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<GOAL>e.toPartialHomeomorph.source = Set.univ
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<GOAL>↑e.toPartialHomeomorph = ⇑e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<GOAL>e.toPartialHomeomorph.target = Set.univ
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : X ≃ₜ Y<GOAL>↑e.toPartialHomeomorph.symm = ⇑e.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>e' : PartialEquiv X Y<VAR>h : e.toPartialEquiv = e'<GOAL>e.replaceEquiv e' h = e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>e.source ⊆ ↑e ⁻¹' e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e e' : PartialHomeomorph X Y<VAR>h : e.toPartialEquiv = e'.toPartialEquiv<GOAL>e = e'
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<GOAL>∀ᶠ (y : X) in 𝓝 x, ↑e.symm (↑e y) = y
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : Y<VAR>hx : x ∈ e.target<GOAL>∀ᶠ (y : X) in 𝓝 (↑e.symm x), ↑e.symm (↑e y) = y
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : Y<VAR>hx : x ∈ e.target<GOAL>∀ᶠ (y : Y) in 𝓝 x, ↑e (↑e.symm y) = y
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<GOAL>∀ᶠ (y : Y) in 𝓝 (↑e x), ↑e (↑e.symm y) = y
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<GOAL>∀ᶠ (x' : X) in 𝓝[≠] x, ↑e x' ≠ ↑e x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<VAR>s : Set X<GOAL>𝓝[e.source ∩ s] x = 𝓝[s] x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : Y<VAR>hx : x ∈ e.target<VAR>s : Set Y<GOAL>𝓝[e.target ∩ s] x = 𝓝[s] x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<VAR>h : s ⊆ e.source<GOAL>↑e '' s = e.target ∩ ↑e.symm ⁻¹' s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<GOAL>↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<GOAL>↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set Y<VAR>h : s ⊆ e.target<GOAL>↑e.symm '' s = e.source ∩ ↑e ⁻¹' s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set Y<GOAL>↑e.symm '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' (e.target ∩ s)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<GOAL>e.source ∩ ↑e ⁻¹' (↑e.symm ⁻¹' s) = e.source ∩ s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set Y<GOAL>e.target ∩ ↑e.symm ⁻¹' (↑e ⁻¹' s) = e.target ∩ s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set Y<GOAL>e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>↑e '' e.source = e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>↑e.symm '' e.target = e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e e' : PartialHomeomorph X Y<VAR>h : ∀ (x : X), ↑e x = ↑e' x<VAR>hinv : ∀ (x : Y), ↑e.symm x = ↑e'.symm x<VAR>hs : e.source = e'.source<GOAL>e = e'
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e e' : PartialHomeomorph X Y<GOAL>e = e' ↔ (∀ (x : X), ↑e x = ↑e' x) ∧ (∀ (x : Y), ↑e.symm x = ↑e'.symm x) ∧ e.source = e'.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>e.symm.toPartialEquiv = e.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>e.symm.source = e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>e.symm.target = e.source
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>e.symm.symm = e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Function.Bijective PartialHomeomorph.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>h : x ∈ e.source<GOAL>ContinuousAt (↑e) x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : Y<VAR>h : x ∈ e.target<GOAL>ContinuousAt (↑e.symm) x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<GOAL>Filter.Tendsto (↑e.symm) (𝓝 (↑e x)) (𝓝 x)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<GOAL>Filter.map (↑e) (𝓝 x) = 𝓝 (↑e x)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<GOAL>Filter.map (↑e.symm) (𝓝 (↑e x)) = 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<VAR>s : Set X<VAR>hs : s ∈ 𝓝 x<GOAL>↑e '' s ∈ 𝓝 (↑e x)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<VAR>s : Set X<GOAL>Filter.map (↑e) (𝓝[s] x) = 𝓝[↑e '' (e.source ∩ s)] ↑e x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<VAR>s : Set Y<GOAL>Filter.map (↑e) (𝓝[↑e ⁻¹' s] x) = 𝓝[s] ↑e x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : Y → Prop<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (y : Y) in 𝓝 (↑e x), p y) ↔ ∀ᶠ (x : X) in 𝓝 x, p (↑e x)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : X → Prop<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (y : Y) in 𝓝 (↑e x), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝 x, p x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : Y → Prop<VAR>s : Set X<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p (↑e x)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : X → Prop<VAR>s : Set X<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Z<VAR>x : X<VAR>f : X → Z<VAR>hf : ContinuousWithinAt f s x<VAR>hxe : x ∈ e.source<VAR>ht : t ∈ 𝓝 (f x)<GOAL>↑e.symm ⁻¹' s =ᶠ[𝓝 (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>s : Set Y<VAR>hs : IsOpen s<GOAL>IsOpen (e.source ∩ ↑e ⁻¹' s)