ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>hs : IsOpen s<GOAL>IsOpen (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<VAR>hs : IsOpen s<VAR>hse : s ⊆ e.source<GOAL>IsOpen (↑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 X<VAR>hs : IsOpen s<GOAL>IsOpen (↑e '' (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>t : Set Y<VAR>ht : IsOpen t<VAR>hte : t ⊆ e.target<GOAL>IsOpen (↑e.symm '' t)
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<VAR>t : Set Y<VAR>hs : t ⊆ e.target<GOAL>IsOpen (↑e.symm '' t) ↔ IsOpen 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 X<VAR>hs : s ⊆ e.source<GOAL>IsOpen (↑e '' s) ↔ IsOpen 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<VAR>t : Set Y<VAR>h : e.IsImage s t<GOAL>e.IsImage s 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 X<VAR>t : Set Y<VAR>x : X<VAR>h : e.IsImage s t<VAR>hx : x ∈ e.source<GOAL>↑e x ∈ t ↔ x ∈ 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<VAR>t : Set Y<VAR>h : e.IsImage s t<GOAL>e.symm.IsImage t 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<VAR>t : Set Y<VAR>y : Y<VAR>h : e.IsImage s t<VAR>hy : y ∈ e.target<GOAL>↑e.symm y ∈ s ↔ y ∈ 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 X<VAR>t : Set Y<GOAL>e.symm.IsImage t s ↔ e.IsImage s 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 X<VAR>t : Set Y<VAR>h : e.IsImage s t<GOAL>Set.MapsTo (↑e) (e.source ∩ s) (e.target ∩ 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 X<VAR>t : Set Y<VAR>h : e.IsImage s t<GOAL>Set.MapsTo (↑e.symm) (e.target ∩ t) (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 X<VAR>t : Set Y<VAR>h : e.IsImage s t<GOAL>↑e '' (e.source ∩ s) = e.target ∩ 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 X<VAR>t : Set Y<VAR>h : e.IsImage s t<GOAL>↑e.symm '' (e.target ∩ t) = 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 X<VAR>t : Set Y<GOAL>e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = 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 X<VAR>t : Set Y<GOAL>e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ 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 X<VAR>t : Set Y<GOAL>e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ 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 X<VAR>t : Set Y<GOAL>e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' (e.target ∩ t) = 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 X<VAR>t : Set Y<VAR>h : ↑e '' (e.source ∩ s) = e.target ∩ t<GOAL>e.IsImage s 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 X<VAR>t : Set Y<VAR>h : ↑e.symm '' (e.target ∩ t) = e.source ∩ s<GOAL>e.IsImage s 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 X<VAR>t : Set Y<VAR>h : e.IsImage s t<GOAL>e.IsImage sᶜ 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 X<VAR>t : Set Y<VAR>s' : Set X<VAR>t' : Set Y<VAR>h : e.IsImage s t<VAR>h' : e.IsImage s' t'<GOAL>e.IsImage (s ∩ s') (t ∩ 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 X<VAR>t : Set Y<VAR>s' : Set X<VAR>t' : Set Y<VAR>h : e.IsImage s t<VAR>h' : e.IsImage s' t'<GOAL>e.IsImage (s ∪ s') (t ∪ 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 X<VAR>t : Set Y<VAR>s' : Set X<VAR>t' : Set Y<VAR>h : e.IsImage s t<VAR>h' : e.IsImage s' t'<GOAL>e.IsImage (s \ s') (t \ 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 X<VAR>t : Set Y<VAR>e' : PartialHomeomorph X Y<VAR>(i : X) → Decidable (i ∈ s)<VAR>(i : Y) → Decidable (i ∈ t)<VAR>h : e.IsImage s t<VAR>h' : e'.IsImage s t<GOAL>Set.LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite 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<VAR>s : Set X<VAR>t : Set Y<VAR>e' : PartialHomeomorph X Y<VAR>h : e.IsImage s t<VAR>h' : e'.IsImage s t<VAR>hs : e.source ∩ s = e'.source ∩ s<VAR>Heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)<GOAL>e.target ∩ t = e'.target ∩ 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 X<VAR>t : Set Y<VAR>e' : PartialHomeomorph X Y<VAR>h : e.IsImage s t<VAR>hs : e.source ∩ s = e'.source ∩ s<VAR>Heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)<GOAL>Set.EqOn (↑e.symm) (↑e'.symm) (e.target ∩ 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 X<VAR>t : Set Y<VAR>x : X<VAR>h : e.IsImage s t<VAR>hx : x ∈ e.source<GOAL>Filter.map (↑e) (𝓝[s] x) = 𝓝[t] ↑e 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>t : Set Y<VAR>h : e.IsImage s t<GOAL>e.IsImage (closure s) (closure 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 X<VAR>t : Set Y<VAR>h : e.IsImage s t<GOAL>e.IsImage (interior s) (interior 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 X<VAR>t : Set Y<VAR>h : e.IsImage s t<GOAL>e.IsImage (frontier s) (frontier 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 X<VAR>t : Set Y<VAR>h : e.IsImage s t<GOAL>IsOpen (e.source ∩ s) ↔ IsOpen (e.target ∩ 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 X<VAR>t : Set Y<VAR>h : e.IsImage s t<VAR>hs : IsOpen (e.source ∩ s)<GOAL>(h.restr hs).toPartialEquiv = ⋯.restr
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>e.IsImage e.source 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>hs : Disjoint e.source e'.source<VAR>ht : Disjoint e.target e'.target<GOAL>e.IsImage 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>s : Set Y<GOAL>e.source ∩ ↑e ⁻¹' interior s = e.source ∩ interior (↑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.source ∩ ↑e ⁻¹' closure s = e.source ∩ closure (↑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.source ∩ ↑e ⁻¹' frontier s = e.source ∩ frontier (↑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 X<VAR>hs : IsOpen s<GOAL>(e.restrOpen s hs).toPartialEquiv = e.restr 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<VAR>hs : IsOpen s<GOAL>(e.restrOpen s hs).source = 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 X<GOAL>(e.restr s).source = e.source ∩ interior 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.restr s).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>s : Set X<GOAL>↑(e.restr s) = ↑e
<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.restr s).target = e.target ∩ ↑e.symm ⁻¹' interior 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.restr s).toPartialEquiv = e.restr (interior 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<VAR>hs : IsOpen s<GOAL>(e.restr s).source = 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 X<VAR>hs : IsOpen s<GOAL>(e.restr s).toPartialEquiv = e.restr 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<VAR>h : e.source ⊆ s<GOAL>e.restr s = e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>e.restr Set.univ = e
<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.restr (e.source ∩ s) = e.restr s
<VAR>X : Type u_7<VAR>TopologicalSpace X<GOAL>(PartialHomeomorph.refl X).source = Set.univ
<VAR>X : Type u_7<VAR>TopologicalSpace X<GOAL>(PartialHomeomorph.refl X).target = Set.univ
<VAR>X : Type u_7<VAR>TopologicalSpace X<GOAL>↑(PartialHomeomorph.refl X) = id
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>(PartialHomeomorph.refl X).toPartialEquiv = PartialEquiv.refl X
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>(PartialHomeomorph.refl X).symm = PartialHomeomorph.refl X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>(PartialHomeomorph.ofSet s hs).source = s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>(PartialHomeomorph.ofSet s hs).target = s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>↑(PartialHomeomorph.ofSet s hs) = id
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>(PartialHomeomorph.ofSet s hs).toPartialEquiv = PartialEquiv.ofSet s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>(PartialHomeomorph.ofSet s hs).symm = PartialHomeomorph.ofSet s hs
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>PartialHomeomorph.ofSet Set.univ ⋯ = PartialHomeomorph.refl 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>e' : PartialHomeomorph Y Z<VAR>h : e.target = e'.source<GOAL>(e.trans' e' h).source = e.source
<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>e' : PartialHomeomorph Y Z<VAR>h : e.target = e'.source<GOAL>(e.trans' e' h).target = e'.target
<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>e' : PartialHomeomorph Y Z<VAR>h : e.target = e'.source<GOAL>∀ (a : X), ↑(e.trans' e' h) a = ↑e' (↑e a)
<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>e' : PartialHomeomorph Y Z<VAR>h : e.target = e'.source<GOAL>(e.trans' e' h).toPartialEquiv = e.trans' e'.toPartialEquiv h
<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>e' : PartialHomeomorph Y Z<VAR>h : e.target = e'.source<GOAL>∀ (a : Z), ↑(e.trans' e' h).symm a = ↑e.symm (↑e'.symm a)
<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>e' : PartialHomeomorph Y Z<GOAL>(e.trans e').toPartialEquiv = e.trans e'.toPartialEquiv
<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>e' : PartialHomeomorph Y Z<GOAL>↑(e.trans e') = ↑e' ∘ ↑e
<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>e' : PartialHomeomorph Y Z<GOAL>↑(e.trans e').symm = ↑e.symm ∘ ↑e'.symm
<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>e' : PartialHomeomorph Y Z<VAR>x : X<GOAL>↑(e.trans e') x = ↑e' (↑e 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>e' : PartialHomeomorph Y Z<GOAL>(e.trans e').symm = e'.symm.trans e.symm
<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>e' : PartialHomeomorph Y Z<GOAL>(e.trans e').source = e.source ∩ ↑e ⁻¹' e'.source
<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>e' : PartialHomeomorph Y Z<GOAL>(e.trans e').source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)
<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>e' : PartialHomeomorph Y Z<GOAL>(e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)
<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>e' : PartialHomeomorph Y Z<GOAL>↑e '' (e.trans e').source = e.target ∩ e'.source
<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>e' : PartialHomeomorph Y Z<GOAL>(e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' e.target
<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>e' : PartialHomeomorph Y Z<GOAL>(e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' (e'.source ∩ e.target)
<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>e' : PartialHomeomorph Y Z<GOAL>(e.trans e').target = ↑e' '' (e'.source ∩ e.target)
<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>e' : PartialHomeomorph Y Z<GOAL>↑e'.symm '' (e.trans e').target = e'.source ∩ e.target
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>e' : PartialHomeomorph Y Z<VAR>e'' : PartialHomeomorph Z Z'<GOAL>(e.trans e').trans e'' = e.trans (e'.trans e'')
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>e.trans (PartialHomeomorph.refl Y) = e
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<GOAL>(PartialHomeomorph.refl X).trans e = e
<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>e.trans (PartialHomeomorph.ofSet s hs) = e.restr (↑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<VAR>hs : IsOpen s<GOAL>e.trans (PartialHomeomorph.ofSet s hs) = e.restr (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 X<VAR>hs : IsOpen s<GOAL>(PartialHomeomorph.ofSet s hs).trans e = e.restr 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<VAR>hs : IsOpen s<GOAL>(PartialHomeomorph.ofSet s hs).trans e = e.restr (e.source ∩ s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>s' : Set X<VAR>hs' : IsOpen s'<GOAL>(PartialHomeomorph.ofSet s hs).trans (PartialHomeomorph.ofSet s' hs') = PartialHomeomorph.ofSet (s ∩ s') ⋯
<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>e' : PartialHomeomorph Y Z<VAR>s : Set X<GOAL>(e.restr s).trans e' = (e.trans e').restr s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e e' : PartialHomeomorph X Y<GOAL>e.EqOnSource e' ↔ e.EqOnSource e'.toPartialEquiv
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e : PartialHomeomorph X Y<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<VAR>h : e ≈ e'<GOAL>e.symm ≈ e'.symm
<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 ≈ e'<GOAL>e.source = 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 : e ≈ e'<GOAL>e.target = 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 ≈ e'<GOAL>Set.EqOn (↑e) (↑e') 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 : e ≈ e'<GOAL>Set.EqOn (↑e.symm) (↑e'.symm) e.target
<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 e' : PartialHomeomorph X Y<VAR>f f' : PartialHomeomorph Y Z<VAR>he : e ≈ e'<VAR>hf : f ≈ f'<GOAL>e.trans f ≈ e'.trans f'
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e e' : PartialHomeomorph X Y<VAR>he : e ≈ e'<VAR>s : Set X<GOAL>e.restr s ≈ e'.restr s
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e e' : PartialHomeomorph X Y<VAR>h : Set.EqOn (↑e) (↑e') (e.source ∩ e'.source)<GOAL>e.restr e'.source ≈ e'.restr 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.trans e.symm ≈ PartialHomeomorph.ofSet 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.trans e ≈ PartialHomeomorph.ofSet 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 ≈ e'<VAR>s : e.source = Set.univ<VAR>t : e.target = Set.univ<GOAL>e = e'
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y<VAR>TopologicalSpace Y'<VAR>eX : PartialHomeomorph X X'<VAR>eY : PartialHomeomorph Y Y'<GOAL>(eX.prod eY).source = eX.source ×ˢ eY.source
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y<VAR>TopologicalSpace Y'<VAR>eX : PartialHomeomorph X X'<VAR>eY : PartialHomeomorph Y Y'<VAR>p : X' × Y'<GOAL>↑(eX.prod eY).symm p = (↑eX.symm p.1, ↑eY.symm p.2)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y<VAR>TopologicalSpace Y'<VAR>eX : PartialHomeomorph X X'<VAR>eY : PartialHomeomorph Y Y'<GOAL>(eX.prod eY).target = eX.target ×ˢ eY.target
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y<VAR>TopologicalSpace Y'<VAR>eX : PartialHomeomorph X X'<VAR>eY : PartialHomeomorph Y Y'<GOAL>↑(eX.prod eY) = fun p => (↑eX p.1, ↑eY p.2)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y<VAR>TopologicalSpace Y'<VAR>eX : PartialHomeomorph X X'<VAR>eY : PartialHomeomorph Y Y'<GOAL>(eX.prod eY).toPartialEquiv = eX.prod eY.toPartialEquiv
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y<VAR>TopologicalSpace Y'<VAR>eX : PartialHomeomorph X X'<VAR>eY : PartialHomeomorph Y Y'<GOAL>(eX.prod eY).symm = eX.symm.prod eY.symm
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>(PartialHomeomorph.refl X).prod (PartialHomeomorph.refl Y) = PartialHomeomorph.refl (X × Y)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y<VAR>TopologicalSpace Y'<VAR>TopologicalSpace Z<VAR>TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : PartialHomeomorph Y Z<VAR>e' : PartialHomeomorph X' Y'<VAR>f' : PartialHomeomorph Y' Z'<GOAL>(e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y<VAR>TopologicalSpace Y'<VAR>eX eX' : PartialHomeomorph X X'<VAR>eY eY' : PartialHomeomorph Y Y'<VAR>h : (eX.prod eY).source.Nonempty<GOAL>eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace X'<VAR>TopologicalSpace Y<VAR>TopologicalSpace Y'<VAR>eX eX' : PartialHomeomorph X X'<VAR>eY eY' : PartialHomeomorph Y Y'<VAR>h : (eX'.prod eY').source.Nonempty<GOAL>eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
<VAR>ι : Type u_7<VAR>Finite ι<VAR>X : ι → Type u_8<VAR>Y : ι → Type u_9<VAR>(i : ι) → TopologicalSpace (X i)<VAR>(i : ι) → TopologicalSpace (Y i)<VAR>ei : (i : ι) → PartialHomeomorph (X i) (Y i)<GOAL>(PartialHomeomorph.pi ei).toPartialEquiv = PartialEquiv.pi fun i => (ei i).toPartialEquiv
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e e' : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Y<VAR>(x : X) → Decidable (x ∈ s)<VAR>(y : Y) → Decidable (y ∈ t)<VAR>H : e.IsImage s t<VAR>H' : e'.IsImage s t<VAR>Hs : e.source ∩ frontier s = e'.source ∩ frontier s<VAR>Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)<GOAL>(e.piecewise e' s t H H' Hs Heq).toPartialEquiv = e.piecewise e'.toPartialEquiv s t H H'
<VAR>X : Type u_1<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>e e' : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Y<VAR>(x : X) → Decidable (x ∈ s)<VAR>(y : Y) → Decidable (y ∈ t)<VAR>H : e.IsImage s t<VAR>H' : e'.IsImage s t<VAR>Hs : e.source ∩ frontier s = e'.source ∩ frontier s<VAR>Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)<GOAL>↑(e.piecewise e' s t H H' Hs Heq) = s.piecewise ↑e ↑e'