Documentation

Mathlib.Topology.OpenPartialHomeomorph.IsImage

Partial homeomorphisms: Images of sets #

Main definitions #

OpenPartialHomeomorph.IsImage: predicate for when one set is an image of another
OpenPartialHomeomorph.ofSet: the identity on a set s
OpenPartialHomeomorph.EqOnSource: equivalence relation describing the "right" notion of equality for open partial homeomorphisms

Implementation notes #

Most statements are copied from their PartialEquiv versions, although some care is required especially when restricting to subsets, as these should be open subsets.

For design notes, see PartialEquiv.lean.

Local coding conventions #

If a lemma deals with the intersection of a set with either source or target of a PartialEquiv, then it should use e.source ∩ s or e.target ∩ t, not s ∩ e.source or t ∩ e.target.

`OpenPartialHomeomorph.IsImage` relation #

We say that t : Set Y is an image of s : Set X under an open partial homeomorphism e if any of the following equivalent conditions hold:

e '' (e.source ∩ s) = e.target ∩ t;
e.source ∩ e ⁻¹ t = e.source ∩ s;
∀ x ∈ e.source, e x ∈ t ↔ x ∈ s (this one is used in the definition).

This definition is a restatement of PartialEquiv.IsImage for open partial homeomorphisms. In this section we transfer API about PartialEquiv.IsImage to open partial homeomorphisms and add a few OpenPartialHomeomorph-specific lemmas like OpenPartialHomeomorph.IsImage.closure.

def OpenPartialHomeomorph.IsImage {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) :

We say that t : Set Y is an image of s : Set X under an open partial homeomorphism e if any of the following equivalent conditions hold:

e '' (e.source ∩ s) = e.target ∩ t;
e.source ∩ e ⁻¹ t = e.source ∩ s;
∀ x ∈ e.source, e x ∈ t ↔ x ∈ s (this one is used in the definition).

Equations

e.IsImage s t = ∀ ⦃x : X⦄, x ∈ e.source → (↑e x ∈ t ↔ x ∈ s)

Instances For

theorem OpenPartialHomeomorph.IsImage.toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

theorem OpenPartialHomeomorph.IsImage.apply_mem_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {x : X} (h : e.IsImage s t) (hx : x ∈ e.source) :

↑e x ∈ t ↔ x ∈ s

theorem OpenPartialHomeomorph.IsImage.symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

e.symm.IsImage t s

theorem OpenPartialHomeomorph.IsImage.symm_apply_mem_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {y : Y} (h : e.IsImage s t) (hy : y ∈ e.target) :

↑e.symm y ∈ s ↔ y ∈ t

@[simp]

theorem OpenPartialHomeomorph.IsImage.symm_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.symm.IsImage t s ↔ e.IsImage s t

theorem OpenPartialHomeomorph.IsImage.mapsTo {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

Set.MapsTo (↑e) (e.source ∩ s) (e.target ∩ t)

theorem OpenPartialHomeomorph.IsImage.symm_mapsTo {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

Set.MapsTo (↑e.symm) (e.target ∩ t) (e.source ∩ s)

theorem OpenPartialHomeomorph.IsImage.image_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

↑e '' (e.source ∩ s) = e.target ∩ t

theorem OpenPartialHomeomorph.IsImage.symm_image_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

↑e.symm '' (e.target ∩ t) = e.source ∩ s

theorem OpenPartialHomeomorph.IsImage.iff_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s

theorem OpenPartialHomeomorph.IsImage.preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.IsImage s t → e.source ∩ ↑e ⁻¹' t = e.source ∩ s

Alias of the forward direction of OpenPartialHomeomorph.IsImage.iff_preimage_eq.

theorem OpenPartialHomeomorph.IsImage.of_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.source ∩ ↑e ⁻¹' t = e.source ∩ s → e.IsImage s t

Alias of the reverse direction of OpenPartialHomeomorph.IsImage.iff_preimage_eq.

theorem OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t

theorem OpenPartialHomeomorph.IsImage.of_symm_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t → e.IsImage s t

Alias of the reverse direction of OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq.

theorem OpenPartialHomeomorph.IsImage.symm_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t

Alias of the forward direction of OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq.

theorem OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t

theorem OpenPartialHomeomorph.IsImage.of_symm_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t → e.IsImage s t

Alias of the reverse direction of OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq'.

theorem OpenPartialHomeomorph.IsImage.symm_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t

Alias of the forward direction of OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq'.

theorem OpenPartialHomeomorph.IsImage.iff_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s

theorem OpenPartialHomeomorph.IsImage.preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.IsImage s t → e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s

Alias of the forward direction of OpenPartialHomeomorph.IsImage.iff_preimage_eq'.

theorem OpenPartialHomeomorph.IsImage.of_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} :

e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s → e.IsImage s t

Alias of the reverse direction of OpenPartialHomeomorph.IsImage.iff_preimage_eq'.

theorem OpenPartialHomeomorph.IsImage.of_image_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : ↑e '' (e.source ∩ s) = e.target ∩ t) :

theorem OpenPartialHomeomorph.IsImage.of_symm_image_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : ↑e.symm '' (e.target ∩ t) = e.source ∩ s) :

theorem OpenPartialHomeomorph.IsImage.compl {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

e.IsImage sᶜ tᶜ

theorem OpenPartialHomeomorph.IsImage.inter {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {s' : Set X} {t' : Set Y} (h : e.IsImage s t) (h' : e.IsImage s' t') :

e.IsImage (s ∩ s') (t ∩ t')

theorem OpenPartialHomeomorph.IsImage.union {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {s' : Set X} {t' : Set Y} (h : e.IsImage s t) (h' : e.IsImage s' t') :

e.IsImage (s ∪ s') (t ∪ t')

theorem OpenPartialHomeomorph.IsImage.diff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {s' : Set X} {t' : Set Y} (h : e.IsImage s t) (h' : e.IsImage s' t') :

e.IsImage (s \ s') (t \ t')

theorem OpenPartialHomeomorph.IsImage.leftInvOn_piecewise {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y} [(i : X) → Decidable (i ∈ s)] [(i : Y) → Decidable (i ∈ t)] (h : e.IsImage s t) (h' : e'.IsImage s t) :

Set.LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)

theorem OpenPartialHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y} (h : e.IsImage s t) (h' : e'.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)) :

e.target ∩ t = e'.target ∩ t

theorem OpenPartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y} (h : e.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)) :

Set.EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)

theorem OpenPartialHomeomorph.IsImage.map_nhdsWithin_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {x : X} (h : e.IsImage s t) (hx : x ∈ e.source) :

Filter.map (↑e) (nhdsWithin x s) = nhdsWithin (↑e x) t

theorem OpenPartialHomeomorph.IsImage.closure {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

e.IsImage (closure s) (closure t)

theorem OpenPartialHomeomorph.IsImage.interior {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

e.IsImage (interior s) (interior t)

theorem OpenPartialHomeomorph.IsImage.frontier {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

e.IsImage (frontier s) (frontier t)

theorem OpenPartialHomeomorph.IsImage.isOpen_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) :

IsOpen (e.source ∩ s) ↔ IsOpen (e.target ∩ t)

def OpenPartialHomeomorph.IsImage.restr {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) :

OpenPartialHomeomorph X Y

Restrict an OpenPartialHomeomorph to a pair of corresponding open sets.

Equations

h.restr hs = { toPartialEquiv := ⋯.restr, open_source := hs, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

Instances For

@[simp]

theorem OpenPartialHomeomorph.IsImage.restr_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) :

↑(h.restr hs) = ↑e

@[simp]

theorem OpenPartialHomeomorph.IsImage.restr_symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) :

↑(h.restr hs).symm = ↑e.symm

@[simp]

theorem OpenPartialHomeomorph.IsImage.restr_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) :

(h.restr hs).toPartialEquiv = ⋯.restr

theorem OpenPartialHomeomorph.isImage_source_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) :

e.IsImage e.source e.target

theorem OpenPartialHomeomorph.isImage_source_target_of_disjoint {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) :

e.IsImage e'.source e'.target

theorem OpenPartialHomeomorph.preimage_interior {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) :

e.source ∩ ↑e ⁻¹' interior s = e.source ∩ interior (↑e ⁻¹' s)

Preimage of interior or interior of preimage coincide for open partial homeomorphisms, when restricted to the source.

theorem OpenPartialHomeomorph.preimage_closure {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) :

e.source ∩ ↑e ⁻¹' closure s = e.source ∩ closure (↑e ⁻¹' s)

theorem OpenPartialHomeomorph.preimage_frontier {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) :

e.source ∩ ↑e ⁻¹' frontier s = e.source ∩ frontier (↑e ⁻¹' s)

Restriction #

def OpenPartialHomeomorph.restrOpen {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) :

OpenPartialHomeomorph X Y

Restricting an open partial homeomorphism e to e.source ∩ s when s is open. This is sometimes hard to use because of the openness assumption, but it has the advantage that when it can be used then its PartialEquiv is defeq to PartialEquiv.restr.

Equations

e.restrOpen s hs = ⋯.restr ⋯

Instances For

@[simp]

theorem OpenPartialHomeomorph.restrOpen_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) :

(e.restrOpen s hs).toPartialEquiv = e.restr s

theorem OpenPartialHomeomorph.restrOpen_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) :

(e.restrOpen s hs).source = e.source ∩ s

@[simp]

theorem OpenPartialHomeomorph.coe_restrOpen {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) :

↑(e.restrOpen s hs) = ↑e

@[simp]

theorem OpenPartialHomeomorph.coe_restrOpen_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) :

↑(e.restrOpen s hs).symm = ↑e.symm

def OpenPartialHomeomorph.restr {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) :

OpenPartialHomeomorph X Y

Restricting an open partial homeomorphism e to e.source ∩ interior s. We use the interior to make sure that the restriction is well defined whatever the set s, since open partial homeomorphisms are by definition defined on open sets. In applications where s is open, this coincides with the restriction of partial equivalences.

Equations

e.restr s = e.restrOpen (interior s) ⋯

Instances For

@[simp]

theorem OpenPartialHomeomorph.restr_symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) :

↑(e.restr s).symm = ↑e.symm

@[simp]

theorem OpenPartialHomeomorph.restr_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) :

↑(e.restr s) = ↑e

theorem OpenPartialHomeomorph.restr_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) :

(e.restr s).target = e.target ∩ ↑e.symm ⁻¹' interior s

theorem OpenPartialHomeomorph.restr_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) :

(e.restr s).source = e.source ∩ interior s

@[simp]

theorem OpenPartialHomeomorph.restr_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) :

(e.restr s).toPartialEquiv = e.restr (interior s)

theorem OpenPartialHomeomorph.restr_source' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) :

(e.restr s).source = e.source ∩ s

theorem OpenPartialHomeomorph.restr_toPartialEquiv' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) :

(e.restr s).toPartialEquiv = e.restr s

theorem OpenPartialHomeomorph.restr_eq_of_source_subset {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} (h : e.source ⊆ s) :

e.restr s = e

@[simp]

theorem OpenPartialHomeomorph.restr_univ {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} :

e.restr Set.univ = e

@[simp]

theorem OpenPartialHomeomorph.restr_source_inter {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) :

e.restr (e.source ∩ s) = e.restr s

ofSet #

The identity on a set s

def OpenPartialHomeomorph.ofSet {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) :

OpenPartialHomeomorph X X

The identity partial equivalence on a set s

Equations

OpenPartialHomeomorph.ofSet s hs = { toPartialEquiv := PartialEquiv.ofSet s, open_source := hs, open_target := hs, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

Instances For

@[simp]

theorem OpenPartialHomeomorph.ofSet_apply {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) :

↑(ofSet s hs) = id

theorem OpenPartialHomeomorph.ofSet_target {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) :

(ofSet s hs).target = s

theorem OpenPartialHomeomorph.ofSet_source {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) :

(ofSet s hs).source = s

@[simp]

theorem OpenPartialHomeomorph.ofSet_toPartialEquiv {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) :

(ofSet s hs).toPartialEquiv = PartialEquiv.ofSet s

@[simp]

theorem OpenPartialHomeomorph.ofSet_symm {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) :

(ofSet s hs).symm = ofSet s hs

@[simp]

theorem OpenPartialHomeomorph.ofSet_univ_eq_refl {X : Type u_1} [TopologicalSpace X] :

ofSet Set.univ ⋯ = OpenPartialHomeomorph.refl X

EqOnSource: equivalence on their source

def OpenPartialHomeomorph.EqOnSource {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) :

EqOnSource e e' means that e and e' have the same source, and coincide there. They should really be considered the same partial equivalence.

Equations

e.EqOnSource e' = (e.source = e'.source ∧ Set.EqOn (↑e) (↑e') e.source)

Instances For

theorem OpenPartialHomeomorph.eqOnSource_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) :

e.EqOnSource e' ↔ e.EqOnSource e'.toPartialEquiv

instance OpenPartialHomeomorph.eqOnSourceSetoid {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] :

Setoid (OpenPartialHomeomorph X Y)

EqOnSource is an equivalence relation.

Equations

OpenPartialHomeomorph.eqOnSourceSetoid = { r := OpenPartialHomeomorph.EqOnSource, iseqv := ⋯ }

theorem OpenPartialHomeomorph.eqOnSource_refl {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) :

e ≈ e

theorem OpenPartialHomeomorph.EqOnSource.symm' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') :

e.symm ≈ e'.symm

If two open partial homeomorphisms are equivalent, so are their inverses.

theorem OpenPartialHomeomorph.EqOnSource.source_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') :

e.source = e'.source

Two equivalent open partial homeomorphisms have the same source.

theorem OpenPartialHomeomorph.EqOnSource.target_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') :

e.target = e'.target

Two equivalent open partial homeomorphisms have the same target.

theorem OpenPartialHomeomorph.EqOnSource.eqOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') :

Set.EqOn (↑e) (↑e') e.source

Two equivalent open partial homeomorphisms have coinciding toFun on the source

theorem OpenPartialHomeomorph.EqOnSource.symm_eqOn_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') :

Set.EqOn (↑e.symm) (↑e'.symm) e.target

Two equivalent open partial homeomorphisms have coinciding invFun on the target

theorem OpenPartialHomeomorph.EqOnSource.restr {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (he : e ≈ e') (s : Set X) :

e.restr s ≈ e'.restr s

Restriction of open partial homeomorphisms respects equivalence

theorem OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : Set.EqOn (↑e) (↑e') (e.source ∩ e'.source)) :

e.restr e'.source ≈ e'.restr e.source

Two equivalent open partial homeomorphisms are equal when the source and target are univ.

theorem OpenPartialHomeomorph.eq_of_eqOnSource_univ {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') (s : e.source = Set.univ) (t : e.target = Set.univ) :

e = e'

theorem OpenPartialHomeomorph.restr_eqOnSource_restr {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s s' : Set X} (hss' : e.source ∩ interior s = e.source ∩ interior s') :

e.restr s ≈ e.restr s'

theorem OpenPartialHomeomorph.restr_inter_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} :

e.restr (e.source ∩ s) ≈ e.restr s

@[simp]

theorem Homeomorph.refl_toOpenPartialHomeomorph {X : Type u_1} [TopologicalSpace X] :

(Homeomorph.refl X).toOpenPartialHomeomorph = OpenPartialHomeomorph.refl X

@[deprecated Homeomorph.refl_toOpenPartialHomeomorph (since := "2025-08-29")]

theorem Homeomorph.refl_toPartialHomeomorph {X : Type u_1} [TopologicalSpace X] :

(Homeomorph.refl X).toOpenPartialHomeomorph = OpenPartialHomeomorph.refl X

Alias of Homeomorph.refl_toOpenPartialHomeomorph.

@[simp]

theorem Homeomorph.symm_toOpenPartialHomeomorph {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) :

e.symm.toOpenPartialHomeomorph = e.toOpenPartialHomeomorph.symm

@[deprecated Homeomorph.symm_toOpenPartialHomeomorph (since := "2025-08-29")]

theorem Homeomorph.symm_toPartialHomeomorph {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) :

e.symm.toOpenPartialHomeomorph = e.toOpenPartialHomeomorph.symm

Alias of Homeomorph.symm_toOpenPartialHomeomorph.