Documentation

Mathlib.Logic.Equiv.PartialEquiv

Partial equivalences #

This files defines equivalences between subsets of given types. An element e of PartialEquiv α β is made of two maps e.toFun and e.invFun respectively from α to β and from β to α (just like equivs), which are inverse to each other on the subsets e.source and e.target of respectively α and β.

They are designed in particular to define charts on manifolds.

The main functionality is e.trans f, which composes the two partial equivalences by restricting the source and target to the maximal set where the composition makes sense.

As for equivs, we register a coercion to functions and use it in our simp normal form: we write e x and e.symm y instead of e.toFun x and e.invFun y.

Main definitions #

Implementation notes #

There are at least three possible implementations of partial equivalences:

Each of these implementations has pros and cons.

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.

Implementation of the mfld_set_tac tactic for working with the domains of partially-defined functions (PartialEquiv, PartialHomeomorph, etc).

This is in a separate file from Mathlib.Logic.Equiv.MfldSimpsAttr because attributes need a new file to become functional.

Common @[simps] configuration options used for manifold-related declarations.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    A very basic tactic to show that sets showing up in manifolds coincide or are included in one another.

    Equations
    Instances For
      structure PartialEquiv (α : Type u_5) (β : Type u_6) :
      Type (max u_5 u_6)

      Local equivalence between subsets source and target of α and β respectively. The (global) maps toFun : α → β and invFun : β → α map source to target and conversely, and are inverse to each other there. The values of toFun outside of source and of invFun outside of target are irrelevant.

      • toFun : αβ

        The global function which has a partial inverse. Its value outside of the source subset is irrelevant.

      • invFun : βα

        The partial inverse to toFun. Its value outside of the target subset is irrelevant.

      • source : Set α

        The domain of the partial equivalence.

      • target : Set β

        The codomain of the partial equivalence.

      • map_source' : ∀ ⦃x : α⦄, x self.sourceself x self.target

        The proposition that elements of source are mapped to elements of target.

      • map_target' : ∀ ⦃x : β⦄, x self.targetself.invFun x self.source

        The proposition that elements of target are mapped to elements of source.

      • left_inv' : ∀ ⦃x : α⦄, x self.sourceself.invFun (self x) = x

        The proposition that invFun is a left-inverse of toFun on source.

      • right_inv' : ∀ ⦃x : β⦄, x self.targetself (self.invFun x) = x

        The proposition that invFun is a right-inverse of toFun on target.

      Instances For
        theorem PartialEquiv.map_source' {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : α :
        x self.sourceself x self.target

        The proposition that elements of source are mapped to elements of target.

        theorem PartialEquiv.map_target' {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : β :
        x self.targetself.invFun x self.source

        The proposition that elements of target are mapped to elements of source.

        theorem PartialEquiv.left_inv' {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : α :
        x self.sourceself.invFun (self x) = x

        The proposition that invFun is a left-inverse of toFun on source.

        theorem PartialEquiv.right_inv' {α : Type u_5} {β : Type u_6} (self : PartialEquiv α β) ⦃x : β :
        x self.targetself (self.invFun x) = x

        The proposition that invFun is a right-inverse of toFun on target.

        instance PartialEquiv.instInhabited {α : Type u_1} {β : Type u_2} [Inhabited α] [Inhabited β] :
        Equations
        • One or more equations did not get rendered due to their size.
        def PartialEquiv.symm {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :

        The inverse of a partial equivalence

        Equations
        • e.symm = { toFun := e.invFun, invFun := e, source := e.target, target := e.source, map_source' := , map_target' := , left_inv' := , right_inv' := }
        Instances For
          instance PartialEquiv.instCoeFunForall {α : Type u_1} {β : Type u_2} :
          CoeFun (PartialEquiv α β) fun (x : PartialEquiv α β) => αβ
          Equations
          • PartialEquiv.instCoeFunForall = { coe := PartialEquiv.toFun }
          def PartialEquiv.Simps.symm_apply {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
          βα

          See Note [custom simps projection]

          Equations
          Instances For
            @[simp]
            theorem PartialEquiv.coe_symm_mk {α : Type u_1} {β : Type u_2} (f : αβ) (g : βα) (s : Set α) (t : Set β) (ml : ∀ ⦃x : α⦄, x sf x t) (mr : ∀ ⦃x : β⦄, x tg x s) (il : ∀ ⦃x : α⦄, x sg (f x) = x) (ir : ∀ ⦃x : β⦄, x tf (g x) = x) :
            { toFun := f, invFun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il, right_inv' := ir }.symm = g
            @[simp]
            theorem PartialEquiv.invFun_as_coe {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
            e.invFun = e.symm
            @[simp]
            theorem PartialEquiv.map_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α} (h : x e.source) :
            e x e.target
            theorem PartialEquiv.map_source'' {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
            e '' e.source e.target

            Variant of e.map_source and map_source', stated for images of subsets of source.

            @[simp]
            theorem PartialEquiv.map_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : β} (h : x e.target) :
            e.symm x e.source
            @[simp]
            theorem PartialEquiv.left_inv {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α} (h : x e.source) :
            e.symm (e x) = x
            @[simp]
            theorem PartialEquiv.right_inv {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : β} (h : x e.target) :
            e (e.symm x) = x
            theorem PartialEquiv.eq_symm_apply {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α} {y : β} (hx : x e.source) (hy : y e.target) :
            x = e.symm y e x = y
            theorem PartialEquiv.mapsTo {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
            Set.MapsTo (e) e.source e.target
            theorem PartialEquiv.symm_mapsTo {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
            Set.MapsTo (e.symm) e.target e.source
            theorem PartialEquiv.leftInvOn {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
            Set.LeftInvOn (e.symm) (e) e.source
            theorem PartialEquiv.rightInvOn {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
            Set.RightInvOn (e.symm) (e) e.target
            theorem PartialEquiv.invOn {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
            Set.InvOn (e.symm) (e) e.source e.target
            theorem PartialEquiv.injOn {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
            Set.InjOn (e) e.source
            theorem PartialEquiv.bijOn {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
            Set.BijOn (e) e.source e.target
            theorem PartialEquiv.surjOn {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
            Set.SurjOn (e) e.source e.target
            @[simp]
            theorem Equiv.toPartialEquivOfImageEq_source {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) (h : e '' s = t) :
            (e.toPartialEquivOfImageEq s t h).source = s
            @[simp]
            theorem Equiv.toPartialEquivOfImageEq_apply {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) (h : e '' s = t) :
            (e.toPartialEquivOfImageEq s t h) = e
            @[simp]
            theorem Equiv.toPartialEquivOfImageEq_target {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) (h : e '' s = t) :
            (e.toPartialEquivOfImageEq s t h).target = t
            @[simp]
            theorem Equiv.toPartialEquivOfImageEq_symm_apply {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) (h : e '' s = t) :
            (e.toPartialEquivOfImageEq s t h).symm = e.symm
            def Equiv.toPartialEquivOfImageEq {α : Type u_1} {β : Type u_2} (e : α β) (s : Set α) (t : Set β) (h : e '' s = t) :

            Interpret an Equiv as a PartialEquiv by restricting it to s in the domain and to t in the codomain.

            Equations
            • e.toPartialEquivOfImageEq s t h = { toFun := e, invFun := e.symm, source := s, target := t, map_source' := , map_target' := , left_inv' := , right_inv' := }
            Instances For
              @[simp]
              theorem Equiv.toPartialEquiv_symm_apply {α : Type u_1} {β : Type u_2} (e : α β) :
              e.toPartialEquiv.symm = e.symm
              @[simp]
              theorem Equiv.toPartialEquiv_target {α : Type u_1} {β : Type u_2} (e : α β) :
              e.toPartialEquiv.target = Set.univ
              @[simp]
              theorem Equiv.toPartialEquiv_apply {α : Type u_1} {β : Type u_2} (e : α β) :
              e.toPartialEquiv = e
              @[simp]
              theorem Equiv.toPartialEquiv_source {α : Type u_1} {β : Type u_2} (e : α β) :
              e.toPartialEquiv.source = Set.univ
              def Equiv.toPartialEquiv {α : Type u_1} {β : Type u_2} (e : α β) :

              Associate a PartialEquiv to an Equiv.

              Equations
              • e.toPartialEquiv = e.toPartialEquivOfImageEq Set.univ Set.univ
              Instances For
                instance PartialEquiv.inhabitedOfEmpty {α : Type u_1} {β : Type u_2} [IsEmpty α] [IsEmpty β] :
                Equations
                @[simp]
                theorem PartialEquiv.copy_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : αβ) (hf : e = f) (g : βα) (hg : e.symm = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
                (e.copy f hf g hg s hs t ht).source = s
                @[simp]
                theorem PartialEquiv.copy_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : αβ) (hf : e = f) (g : βα) (hg : e.symm = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
                (e.copy f hf g hg s hs t ht).target = t
                @[simp]
                theorem PartialEquiv.copy_apply {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : αβ) (hf : e = f) (g : βα) (hg : e.symm = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
                (e.copy f hf g hg s hs t ht) = f
                @[simp]
                theorem PartialEquiv.copy_symm_apply {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : αβ) (hf : e = f) (g : βα) (hg : e.symm = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
                (e.copy f hf g hg s hs t ht).symm = g
                def PartialEquiv.copy {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : αβ) (hf : e = f) (g : βα) (hg : e.symm = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :

                Create a copy of a PartialEquiv providing better definitional equalities.

                Equations
                • e.copy f hf g hg s hs t ht = { toFun := f, invFun := g, source := s, target := t, map_source' := , map_target' := , left_inv' := , right_inv' := }
                Instances For
                  theorem PartialEquiv.copy_eq {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : αβ) (hf : e = f) (g : βα) (hg : e.symm = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
                  e.copy f hf g hg s hs t ht = e
                  def PartialEquiv.toEquiv {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                  e.source e.target

                  Associate to a PartialEquiv an Equiv between the source and the target.

                  Equations
                  • e.toEquiv = { toFun := fun (x : e.source) => e x, , invFun := fun (y : e.target) => e.symm y, , left_inv := , right_inv := }
                  Instances For
                    @[simp]
                    theorem PartialEquiv.symm_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                    e.symm.source = e.target
                    @[simp]
                    theorem PartialEquiv.symm_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                    e.symm.target = e.source
                    @[simp]
                    theorem PartialEquiv.symm_symm {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                    e.symm.symm = e
                    theorem PartialEquiv.symm_bijective {α : Type u_1} {β : Type u_2} :
                    Function.Bijective PartialEquiv.symm
                    theorem PartialEquiv.image_source_eq_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                    e '' e.source = e.target
                    theorem PartialEquiv.forall_mem_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {p : βProp} :
                    (ye.target, p y) xe.source, p (e x)
                    theorem PartialEquiv.exists_mem_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {p : βProp} :
                    (ye.target, p y) xe.source, p (e x)
                    def PartialEquiv.IsImage {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α) (t : Set β) :

                    We say that t : Set β is an image of s : Set α under a partial equivalence 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 e.source(e x t x s)
                    Instances For
                      theorem PartialEquiv.IsImage.apply_mem_iff {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {x : α} (h : e.IsImage s t) (hx : x e.source) :
                      e x t x s
                      theorem PartialEquiv.IsImage.symm_apply_mem_iff {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) ⦃y : β :
                      y e.target(e.symm y s y t)
                      theorem PartialEquiv.IsImage.symm {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :
                      e.symm.IsImage t s
                      @[simp]
                      theorem PartialEquiv.IsImage.symm_iff {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} :
                      e.symm.IsImage t s e.IsImage s t
                      theorem PartialEquiv.IsImage.mapsTo {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :
                      Set.MapsTo (e) (e.source s) (e.target t)
                      theorem PartialEquiv.IsImage.symm_mapsTo {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :
                      Set.MapsTo (e.symm) (e.target t) (e.source s)
                      @[simp]
                      theorem PartialEquiv.IsImage.restr_source {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :
                      h.restr.source = e.source s
                      @[simp]
                      theorem PartialEquiv.IsImage.restr_apply {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :
                      h.restr = e
                      @[simp]
                      theorem PartialEquiv.IsImage.restr_target {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :
                      h.restr.target = e.target t
                      @[simp]
                      theorem PartialEquiv.IsImage.restr_symm_apply {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :
                      h.restr.symm = e.symm
                      def PartialEquiv.IsImage.restr {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :

                      Restrict a PartialEquiv to a pair of corresponding sets.

                      Equations
                      • h.restr = { toFun := e, invFun := e.symm, source := e.source s, target := e.target t, map_source' := , map_target' := , left_inv' := , right_inv' := }
                      Instances For
                        theorem PartialEquiv.IsImage.image_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :
                        e '' (e.source s) = e.target t
                        theorem PartialEquiv.IsImage.symm_image_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :
                        e.symm '' (e.target t) = e.source s
                        theorem PartialEquiv.IsImage.iff_preimage_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} :
                        e.IsImage s t e.source e ⁻¹' t = e.source s
                        theorem PartialEquiv.IsImage.preimage_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} :
                        e.IsImage s te.source e ⁻¹' t = e.source s

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

                        theorem PartialEquiv.IsImage.of_preimage_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} :
                        e.source e ⁻¹' t = e.source se.IsImage s t

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

                        theorem PartialEquiv.IsImage.iff_symm_preimage_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} :
                        e.IsImage s t e.target e.symm ⁻¹' s = e.target t
                        theorem PartialEquiv.IsImage.symm_preimage_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} :
                        e.IsImage s te.target e.symm ⁻¹' s = e.target t

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

                        theorem PartialEquiv.IsImage.of_symm_preimage_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} :
                        e.target e.symm ⁻¹' s = e.target te.IsImage s t

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

                        theorem PartialEquiv.IsImage.of_image_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e '' (e.source s) = e.target t) :
                        e.IsImage s t
                        theorem PartialEquiv.IsImage.of_symm_image_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.symm '' (e.target t) = e.source s) :
                        e.IsImage s t
                        theorem PartialEquiv.IsImage.compl {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t) :
                        e.IsImage s t
                        theorem PartialEquiv.IsImage.inter {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β} (h : e.IsImage s t) (h' : e.IsImage s' t') :
                        e.IsImage (s s') (t t')
                        theorem PartialEquiv.IsImage.union {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β} (h : e.IsImage s t) (h' : e.IsImage s' t') :
                        e.IsImage (s s') (t t')
                        theorem PartialEquiv.IsImage.diff {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β} (h : e.IsImage s t) (h' : e.IsImage s' t') :
                        e.IsImage (s \ s') (t \ t')
                        theorem PartialEquiv.IsImage.leftInvOn_piecewise {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {e' : PartialEquiv α β} [(i : α) → Decidable (i s)] [(i : β) → 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 PartialEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {e' : PartialEquiv α β} (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 PartialEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {e' : PartialEquiv α β} (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 PartialEquiv.isImage_source_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                        e.IsImage e.source e.target
                        theorem PartialEquiv.isImage_source_target_of_disjoint {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) :
                        e.IsImage e'.source e'.target
                        theorem PartialEquiv.image_source_inter_eq' {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α) :
                        e '' (e.source s) = e.target e.symm ⁻¹' s
                        theorem PartialEquiv.image_source_inter_eq {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α) :
                        e '' (e.source s) = e.target e.symm ⁻¹' (e.source s)
                        theorem PartialEquiv.image_eq_target_inter_inv_preimage {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set α} (h : s e.source) :
                        e '' s = e.target e.symm ⁻¹' s
                        theorem PartialEquiv.symm_image_eq_source_inter_preimage {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set β} (h : s e.target) :
                        e.symm '' s = e.source e ⁻¹' s
                        theorem PartialEquiv.symm_image_target_inter_eq {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β) :
                        e.symm '' (e.target s) = e.source e ⁻¹' (e.target s)
                        theorem PartialEquiv.symm_image_target_inter_eq' {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β) :
                        e.symm '' (e.target s) = e.source e ⁻¹' s
                        theorem PartialEquiv.source_inter_preimage_inv_preimage {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α) :
                        e.source e ⁻¹' (e.symm ⁻¹' s) = e.source s
                        theorem PartialEquiv.source_inter_preimage_target_inter {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β) :
                        e.source e ⁻¹' (e.target s) = e.source e ⁻¹' s
                        theorem PartialEquiv.target_inter_inv_preimage_preimage {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β) :
                        e.target e.symm ⁻¹' (e ⁻¹' s) = e.target s
                        theorem PartialEquiv.symm_image_image_of_subset_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set α} (h : s e.source) :
                        e.symm '' (e '' s) = s
                        theorem PartialEquiv.image_symm_image_of_subset_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set β} (h : s e.target) :
                        e '' (e.symm '' s) = s
                        theorem PartialEquiv.source_subset_preimage_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                        e.source e ⁻¹' e.target
                        theorem PartialEquiv.symm_image_target_eq_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                        e.symm '' e.target = e.source
                        theorem PartialEquiv.target_subset_preimage_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                        e.target e.symm ⁻¹' e.source
                        theorem PartialEquiv.ext {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {e' : PartialEquiv α β} (h : ∀ (x : α), e x = e' x) (hsymm : ∀ (x : β), e.symm x = e'.symm x) (hs : e.source = e'.source) :
                        e = e'

                        Two partial equivs that have the same source, same toFun and same invFun, coincide.

                        def PartialEquiv.restr {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α) :

                        Restricting a partial equivalence to e.source ∩ s

                        Equations
                        • e.restr s = .restr
                        Instances For
                          @[simp]
                          theorem PartialEquiv.restr_coe {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α) :
                          (e.restr s) = e
                          @[simp]
                          theorem PartialEquiv.restr_coe_symm {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α) :
                          (e.restr s).symm = e.symm
                          @[simp]
                          theorem PartialEquiv.restr_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α) :
                          (e.restr s).source = e.source s
                          @[simp]
                          theorem PartialEquiv.restr_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α) :
                          (e.restr s).target = e.target e.symm ⁻¹' s
                          theorem PartialEquiv.restr_eq_of_source_subset {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} (h : e.source s) :
                          e.restr s = e
                          @[simp]
                          theorem PartialEquiv.restr_univ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} :
                          e.restr Set.univ = e
                          def PartialEquiv.refl (α : Type u_5) :

                          The identity partial equiv

                          Equations
                          Instances For
                            @[simp]
                            theorem PartialEquiv.refl_source {α : Type u_1} :
                            (PartialEquiv.refl α).source = Set.univ
                            @[simp]
                            theorem PartialEquiv.refl_target {α : Type u_1} :
                            (PartialEquiv.refl α).target = Set.univ
                            @[simp]
                            theorem PartialEquiv.refl_coe {α : Type u_1} :
                            (PartialEquiv.refl α) = id
                            @[simp]
                            theorem PartialEquiv.refl_restr_source {α : Type u_1} (s : Set α) :
                            ((PartialEquiv.refl α).restr s).source = s
                            theorem PartialEquiv.refl_restr_target {α : Type u_1} (s : Set α) :
                            ((PartialEquiv.refl α).restr s).target = s
                            def PartialEquiv.ofSet {α : Type u_1} (s : Set α) :

                            The identity partial equivalence on a set s

                            Equations
                            • PartialEquiv.ofSet s = { toFun := id, invFun := id, source := s, target := s, map_source' := , map_target' := , left_inv' := , right_inv' := }
                            Instances For
                              @[simp]
                              theorem PartialEquiv.ofSet_source {α : Type u_1} (s : Set α) :
                              (PartialEquiv.ofSet s).source = s
                              @[simp]
                              theorem PartialEquiv.ofSet_target {α : Type u_1} (s : Set α) :
                              (PartialEquiv.ofSet s).target = s
                              @[simp]
                              theorem PartialEquiv.ofSet_coe {α : Type u_1} (s : Set α) :
                              @[simp]
                              theorem PartialEquiv.ofSet_symm {α : Type u_1} (s : Set α) :
                              @[simp]
                              theorem PartialEquiv.trans'_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (h : e.target = e'.source) :
                              ∀ (a : α), (e.trans' e' h) a = (e' e) a
                              @[simp]
                              theorem PartialEquiv.trans'_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (h : e.target = e'.source) :
                              (e.trans' e' h).target = e'.target
                              @[simp]
                              theorem PartialEquiv.trans'_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (h : e.target = e'.source) :
                              ∀ (a : γ), (e.trans' e' h).symm a = (e.symm e'.symm) a
                              @[simp]
                              theorem PartialEquiv.trans'_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (h : e.target = e'.source) :
                              (e.trans' e' h).source = e.source
                              def PartialEquiv.trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (h : e.target = e'.source) :

                              Composing two partial equivs if the target of the first coincides with the source of the second.

                              Equations
                              • e.trans' e' h = { toFun := e' e, invFun := e.symm e'.symm, source := e.source, target := e'.target, map_source' := , map_target' := , left_inv' := , right_inv' := }
                              Instances For
                                def PartialEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :

                                Composing two partial equivs, by restricting to the maximal domain where their composition is well defined.

                                Equations
                                • e.trans e' = (e.symm.restr e'.source).symm.trans' (e'.restr e.target)
                                Instances For
                                  @[simp]
                                  theorem PartialEquiv.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  (e.trans e') = e' e
                                  @[simp]
                                  theorem PartialEquiv.coe_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  (e.trans e').symm = e.symm e'.symm
                                  theorem PartialEquiv.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) {x : α} :
                                  (e.trans e') x = e' (e x)
                                  theorem PartialEquiv.trans_symm_eq_symm_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  (e.trans e').symm = e'.symm.trans e.symm
                                  @[simp]
                                  theorem PartialEquiv.trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  (e.trans e').source = e.source e ⁻¹' e'.source
                                  theorem PartialEquiv.trans_source' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  (e.trans e').source = e.source e ⁻¹' (e.target e'.source)
                                  theorem PartialEquiv.trans_source'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  (e.trans e').source = e.symm '' (e.target e'.source)
                                  theorem PartialEquiv.image_trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  e '' (e.trans e').source = e.target e'.source
                                  @[simp]
                                  theorem PartialEquiv.trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  (e.trans e').target = e'.target e'.symm ⁻¹' e.target
                                  theorem PartialEquiv.trans_target' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  (e.trans e').target = e'.target e'.symm ⁻¹' (e'.source e.target)
                                  theorem PartialEquiv.trans_target'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  (e.trans e').target = e' '' (e'.source e.target)
                                  theorem PartialEquiv.inv_image_trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) :
                                  e'.symm '' (e.trans e').target = e'.source e.target
                                  theorem PartialEquiv.trans_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (e'' : PartialEquiv γ δ) :
                                  (e.trans e').trans e'' = e.trans (e'.trans e'')
                                  @[simp]
                                  theorem PartialEquiv.trans_refl {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                                  e.trans (PartialEquiv.refl β) = e
                                  @[simp]
                                  theorem PartialEquiv.refl_trans {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                                  (PartialEquiv.refl α).trans e = e
                                  theorem PartialEquiv.trans_ofSet {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β) :
                                  e.trans (PartialEquiv.ofSet s) = e.restr (e ⁻¹' s)
                                  theorem PartialEquiv.trans_refl_restr {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β) :
                                  e.trans ((PartialEquiv.refl β).restr s) = e.restr (e ⁻¹' s)
                                  theorem PartialEquiv.trans_refl_restr' {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β) :
                                  e.trans ((PartialEquiv.refl β).restr s) = e.restr (e.source e ⁻¹' s)
                                  theorem PartialEquiv.restr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (s : Set α) :
                                  (e.restr s).trans e' = (e.trans e').restr s
                                  theorem PartialEquiv.mem_symm_trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) {e' : PartialEquiv α γ} {x : α} (he : x e.source) (he' : x e'.source) :
                                  e x (e.symm.trans e').source

                                  A lemma commonly useful when e and e' are charts of a manifold.

                                  def PartialEquiv.EqOnSource {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) :

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

                                  Equations
                                  • e.EqOnSource e' = (e.source = e'.source Set.EqOn (e) (e') e.source)
                                  Instances For
                                    instance PartialEquiv.eqOnSourceSetoid {α : Type u_1} {β : Type u_2} :

                                    EqOnSource is an equivalence relation. This instance provides the notation between two PartialEquivs.

                                    Equations
                                    • PartialEquiv.eqOnSourceSetoid = { r := PartialEquiv.EqOnSource, iseqv := }
                                    theorem PartialEquiv.eqOnSource_refl {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                                    e e
                                    theorem PartialEquiv.EqOnSource.source_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {e' : PartialEquiv α β} (h : e e') :
                                    e.source = e'.source

                                    Two equivalent partial equivs have the same source.

                                    theorem PartialEquiv.EqOnSource.eqOn {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {e' : PartialEquiv α β} (h : e e') :
                                    Set.EqOn (e) (e') e.source

                                    Two equivalent partial equivs coincide on the source.

                                    theorem PartialEquiv.EqOnSource.target_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {e' : PartialEquiv α β} (h : e e') :
                                    e.target = e'.target

                                    Two equivalent partial equivs have the same target.

                                    theorem PartialEquiv.EqOnSource.symm' {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {e' : PartialEquiv α β} (h : e e') :
                                    e.symm e'.symm

                                    If two partial equivs are equivalent, so are their inverses.

                                    theorem PartialEquiv.EqOnSource.symm_eqOn {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {e' : PartialEquiv α β} (h : e e') :
                                    Set.EqOn (e.symm) (e'.symm) e.target

                                    Two equivalent partial equivs have coinciding inverses on the target.

                                    theorem PartialEquiv.EqOnSource.trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {e : PartialEquiv α β} {e' : PartialEquiv α β} {f : PartialEquiv β γ} {f' : PartialEquiv β γ} (he : e e') (hf : f f') :
                                    e.trans f e'.trans f'

                                    Composition of partial equivs respects equivalence.

                                    theorem PartialEquiv.EqOnSource.restr {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {e' : PartialEquiv α β} (he : e e') (s : Set α) :
                                    e.restr s e'.restr s

                                    Restriction of partial equivs respects equivalence.

                                    theorem PartialEquiv.EqOnSource.source_inter_preimage_eq {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {e' : PartialEquiv α β} (he : e e') (s : Set β) :
                                    e.source e ⁻¹' s = e'.source e' ⁻¹' s

                                    Preimages are respected by equivalence.

                                    theorem PartialEquiv.self_trans_symm {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                                    e.trans e.symm PartialEquiv.ofSet e.source

                                    Composition of a partial equivlance and its inverse is equivalent to the restriction of the identity to the source.

                                    theorem PartialEquiv.symm_trans_self {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) :
                                    e.symm.trans e PartialEquiv.ofSet e.target

                                    Composition of the inverse of a partial equivalence and this partial equivalence is equivalent to the restriction of the identity to the target.

                                    theorem PartialEquiv.eq_of_eqOnSource_univ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (h : e e') (s : e.source = Set.univ) (t : e.target = Set.univ) :
                                    e = e'

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

                                    def PartialEquiv.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
                                    PartialEquiv (α × γ) (β × δ)

                                    The product of two partial equivalences, as a partial equivalence on the product.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem PartialEquiv.prod_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
                                      (e.prod e').source = e.source ×ˢ e'.source
                                      @[simp]
                                      theorem PartialEquiv.prod_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
                                      (e.prod e').target = e.target ×ˢ e'.target
                                      @[simp]
                                      theorem PartialEquiv.prod_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
                                      (e.prod e') = fun (p : α × γ) => (e p.1, e' p.2)
                                      theorem PartialEquiv.prod_coe_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
                                      (e.prod e').symm = fun (p : β × δ) => (e.symm p.1, e'.symm p.2)
                                      @[simp]
                                      theorem PartialEquiv.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ) :
                                      (e.prod e').symm = e.symm.prod e'.symm
                                      @[simp]
                                      theorem PartialEquiv.refl_prod_refl {α : Type u_1} {β : Type u_2} :
                                      @[simp]
                                      theorem PartialEquiv.prod_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {η : Type u_5} {ε : Type u_6} (e : PartialEquiv α β) (f : PartialEquiv β γ) (e' : PartialEquiv δ η) (f' : PartialEquiv η ε) :
                                      (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
                                      @[simp]
                                      theorem PartialEquiv.piecewise_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (s : Set α) (t : Set β) [(x : α) → Decidable (x s)] [(y : β) → Decidable (y t)] (H : e.IsImage s t) (H' : e'.IsImage s t) :
                                      (e.piecewise e' s t H H').source = s.ite e.source e'.source
                                      @[simp]
                                      theorem PartialEquiv.piecewise_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (s : Set α) (t : Set β) [(x : α) → Decidable (x s)] [(y : β) → Decidable (y t)] (H : e.IsImage s t) (H' : e'.IsImage s t) :
                                      (e.piecewise e' s t H H').target = t.ite e.target e'.target
                                      @[simp]
                                      theorem PartialEquiv.piecewise_symm_apply {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (s : Set α) (t : Set β) [(x : α) → Decidable (x s)] [(y : β) → Decidable (y t)] (H : e.IsImage s t) (H' : e'.IsImage s t) :
                                      (e.piecewise e' s t H H').symm = t.piecewise e.symm e'.symm
                                      @[simp]
                                      theorem PartialEquiv.piecewise_apply {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (s : Set α) (t : Set β) [(x : α) → Decidable (x s)] [(y : β) → Decidable (y t)] (H : e.IsImage s t) (H' : e'.IsImage s t) :
                                      (e.piecewise e' s t H H') = s.piecewise e e'
                                      def PartialEquiv.piecewise {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (s : Set α) (t : Set β) [(x : α) → Decidable (x s)] [(y : β) → Decidable (y t)] (H : e.IsImage s t) (H' : e'.IsImage s t) :

                                      Combine two PartialEquivs using Set.piecewise. The source of the new PartialEquiv is s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s, and similarly for target. The function sends e.source ∩ s to e.target ∩ t using e and e'.source \ s to e'.target \ t using e', and similarly for the inverse function. The definition assumes e.isImage s t and e'.isImage s t.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem PartialEquiv.symm_piecewise {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) {s : Set α} {t : Set β} [(x : α) → Decidable (x s)] [(y : β) → Decidable (y t)] (H : e.IsImage s t) (H' : e'.IsImage s t) :
                                        (e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s
                                        @[simp]
                                        theorem PartialEquiv.disjointUnion_target {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [(x : α) → Decidable (x e.source)] [(y : β) → Decidable (y e.target)] :
                                        (e.disjointUnion e' hs ht).target = e.target e'.target
                                        @[simp]
                                        theorem PartialEquiv.disjointUnion_symm_apply {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [(x : α) → Decidable (x e.source)] [(y : β) → Decidable (y e.target)] :
                                        (e.disjointUnion e' hs ht).symm = e.target.piecewise e.symm e'.symm
                                        @[simp]
                                        theorem PartialEquiv.disjointUnion_source {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [(x : α) → Decidable (x e.source)] [(y : β) → Decidable (y e.target)] :
                                        (e.disjointUnion e' hs ht).source = e.source e'.source
                                        @[simp]
                                        theorem PartialEquiv.disjointUnion_apply {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [(x : α) → Decidable (x e.source)] [(y : β) → Decidable (y e.target)] :
                                        (e.disjointUnion e' hs ht) = e.source.piecewise e e'
                                        def PartialEquiv.disjointUnion {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [(x : α) → Decidable (x e.source)] [(y : β) → Decidable (y e.target)] :

                                        Combine two PartialEquivs with disjoint sources and disjoint targets. We reuse PartialEquiv.piecewise, then override source and target to ensure better definitional equalities.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          theorem PartialEquiv.disjointUnion_eq_piecewise {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [(x : α) → Decidable (x e.source)] [(y : β) → Decidable (y e.target)] :
                                          e.disjointUnion e' hs ht = e.piecewise e' e.source e.target
                                          @[simp]
                                          theorem PartialEquiv.pi_source {ι : Type u_5} {αi : ιType u_6} {βi : ιType u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)) :
                                          (PartialEquiv.pi ei).source = Set.univ.pi fun (i : ι) => (ei i).source
                                          @[simp]
                                          theorem PartialEquiv.pi_target {ι : Type u_5} {αi : ιType u_6} {βi : ιType u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)) :
                                          (PartialEquiv.pi ei).target = Set.univ.pi fun (i : ι) => (ei i).target
                                          @[simp]
                                          theorem PartialEquiv.pi_apply {ι : Type u_5} {αi : ιType u_6} {βi : ιType u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)) :
                                          (PartialEquiv.pi ei) = fun (f : (i : ι) → αi i) (i : ι) => (ei i) (f i)
                                          def PartialEquiv.pi {ι : Type u_5} {αi : ιType u_6} {βi : ιType u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)) :
                                          PartialEquiv ((i : ι) → αi i) ((i : ι) → βi i)

                                          The product of a family of partial equivalences, as a partial equivalence on the pi type.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem PartialEquiv.pi_symm {ι : Type u_5} {αi : ιType u_6} {βi : ιType u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)) :
                                            (PartialEquiv.pi ei).symm = PartialEquiv.pi fun (i : ι) => (ei i).symm
                                            theorem PartialEquiv.pi_symm_apply {ι : Type u_5} {αi : ιType u_6} {βi : ιType u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)) :
                                            (PartialEquiv.pi ei).symm = fun (f : (i : ι) → βi i) (i : ι) => (ei i).symm (f i)
                                            @[simp]
                                            theorem PartialEquiv.pi_refl {ι : Type u_5} {αi : ιType u_6} :
                                            (PartialEquiv.pi fun (i : ι) => PartialEquiv.refl (αi i)) = PartialEquiv.refl ((i : ι) → αi i)
                                            @[simp]
                                            theorem PartialEquiv.pi_trans {ι : Type u_5} {αi : ιType u_6} {βi : ιType u_7} {γi : ιType u_8} (ei : (i : ι) → PartialEquiv (αi i) (βi i)) (ei' : (i : ι) → PartialEquiv (βi i) (γi i)) :
                                            (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = PartialEquiv.pi fun (i : ι) => (ei i).trans (ei' i)
                                            @[simp]
                                            theorem Set.BijOn.toPartialEquiv_target {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) (t : Set β) (hf : Set.BijOn f s t) :
                                            (Set.BijOn.toPartialEquiv f s t hf).target = t
                                            @[simp]
                                            theorem Set.BijOn.toPartialEquiv_symm_apply {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) (t : Set β) (hf : Set.BijOn f s t) :
                                            @[simp]
                                            theorem Set.BijOn.toPartialEquiv_source {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) (t : Set β) (hf : Set.BijOn f s t) :
                                            (Set.BijOn.toPartialEquiv f s t hf).source = s
                                            @[simp]
                                            theorem Set.BijOn.toPartialEquiv_apply {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) (t : Set β) (hf : Set.BijOn f s t) :
                                            (Set.BijOn.toPartialEquiv f s t hf) = f
                                            noncomputable def Set.BijOn.toPartialEquiv {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) (t : Set β) (hf : Set.BijOn f s t) :

                                            A bijection between two sets s : Set α and t : Set β provides a partial equivalence between α and β.

                                            Equations
                                            Instances For
                                              noncomputable def Set.InjOn.toPartialEquiv {α : Type u_1} {β : Type u_2} [Nonempty α] (f : αβ) (s : Set α) (hf : Set.InjOn f s) :

                                              A map injective on a subset of its domain provides a partial equivalence.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem Equiv.refl_toPartialEquiv {α : Type u_1} :
                                                (Equiv.refl α).toPartialEquiv = PartialEquiv.refl α
                                                @[simp]
                                                theorem Equiv.symm_toPartialEquiv {α : Type u_1} {β : Type u_2} (e : α β) :
                                                e.symm.toPartialEquiv = e.toPartialEquiv.symm
                                                @[simp]
                                                theorem Equiv.trans_toPartialEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (e' : β γ) :
                                                (e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv
                                                @[simp]
                                                theorem Equiv.transPartialEquiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f' : PartialEquiv β γ) :
                                                ∀ (a : α), (e.transPartialEquiv f') a = f' (e a)
                                                @[simp]
                                                theorem Equiv.transPartialEquiv_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f' : PartialEquiv β γ) :
                                                (e.transPartialEquiv f').source = e ⁻¹' f'.source
                                                @[simp]
                                                theorem Equiv.transPartialEquiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f' : PartialEquiv β γ) :
                                                ∀ (a : γ), (e.transPartialEquiv f').symm a = e.symm (f'.symm a)
                                                @[simp]
                                                theorem Equiv.transPartialEquiv_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f' : PartialEquiv β γ) :
                                                (e.transPartialEquiv f').target = f'.target
                                                def Equiv.transPartialEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f' : PartialEquiv β γ) :

                                                Precompose a partial equivalence with an equivalence. We modify the source and target to have better definitional behavior.

                                                Equations
                                                • e.transPartialEquiv f' = (e.toPartialEquiv.trans f').copy (e.toPartialEquiv.trans f') (e.toPartialEquiv.trans f').symm (e ⁻¹' f'.source) f'.target
                                                Instances For
                                                  theorem Equiv.transPartialEquiv_eq_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f' : PartialEquiv β γ) :
                                                  e.transPartialEquiv f' = e.toPartialEquiv.trans f'
                                                  @[simp]
                                                  theorem Equiv.transPartialEquiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α β) (f' : PartialEquiv β γ) (f'' : PartialEquiv γ δ) :
                                                  (e.transPartialEquiv f').trans f'' = e.transPartialEquiv (f'.trans f'')
                                                  @[simp]
                                                  theorem Equiv.trans_transPartialEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α β) (e' : β γ) (f'' : PartialEquiv γ δ) :
                                                  (e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'')
                                                  @[simp]
                                                  theorem PartialEquiv.transEquiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (f' : β γ) :
                                                  ∀ (a : α), (e.transEquiv f') a = f' (e a)
                                                  @[simp]
                                                  theorem PartialEquiv.transEquiv_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (f' : β γ) :
                                                  (e.transEquiv f').target = f'.symm ⁻¹' e.target
                                                  @[simp]
                                                  theorem PartialEquiv.transEquiv_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (f' : β γ) :
                                                  (e.transEquiv f').source = e.source
                                                  @[simp]
                                                  theorem PartialEquiv.transEquiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (f' : β γ) :
                                                  ∀ (a : γ), (e.transEquiv f').symm a = e.symm (f'.symm a)
                                                  def PartialEquiv.transEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (f' : β γ) :

                                                  Postcompose a partial equivalence with an equivalence. We modify the source and target to have better definitional behavior.

                                                  Equations
                                                  • e.transEquiv f' = (e.trans f'.toPartialEquiv).copy (e.trans f'.toPartialEquiv) (e.trans f'.toPartialEquiv).symm e.source (f'.symm ⁻¹' e.target)
                                                  Instances For
                                                    theorem PartialEquiv.transEquiv_eq_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : β γ) :
                                                    e.transEquiv e' = e.trans e'.toPartialEquiv
                                                    @[simp]
                                                    theorem PartialEquiv.transEquiv_transEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (f' : β γ) (f'' : γ δ) :
                                                    (e.transEquiv f').transEquiv f'' = e.transEquiv (f'.trans f'')
                                                    @[simp]
                                                    theorem PartialEquiv.trans_transEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (f'' : γ δ) :
                                                    (e.trans e').transEquiv f'' = e.trans (e'.transEquiv f'')