Documentation

Mathlib.Logic.Equiv.LocalEquiv

Local equivalences #

This files defines equivalences between subsets of given types. An element e of LocalEquiv α β 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 local 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 #

Equiv.toLocalEquiv: associating a local equiv to an equiv, with source = target = univ LocalEquiv.symm : the inverse of a local equiv LocalEquiv.trans : the composition of two local equivs LocalEquiv.refl : the identity local equiv LocalEquiv.ofSet : the identity on a set s EqOnSource : equivalence relation describing the "right" notion of equality for local equivs (see below in implementation notes)

Implementation notes #

There are at least three possible implementations of local 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 LocalEquiv, then it should use e.source ∩ s∩ s or e.target ∩ t∩ t, not s ∩ e.source∩ e.source or t ∩ e.target∩ e.target.

Implementation of the mfld_set_tac tactic for working with the domains of partially-defined functions (LocalEquiv, LocalHomeomorph, 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.

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

Equations
structure LocalEquiv (α : Type u_1) (β : Type u_2) :
Type (maxu_1u_2)
  • The global function which has a local inverse. Its value outside of the source subset is irrelevant.

    toFun : αβ
  • The local inverse to toFun. Its value outside of the target subset is irrelevant.

    invFun : βα
  • The domain of the local equivalence.

    source : Set α
  • The codomain of the local equivalence.

    target : Set β
  • The proposition that elements of source are mapped to elements of target.

    map_source' : ∀ ⦃x : α⦄, x sourcetoFun x target
  • The proposition that elements of target are mapped to elements of source.

    map_target' : ∀ ⦃x : β⦄, x targetinvFun x source
  • The proposition that invFun is a local left-inverse of toFun on source.

    left_inv' : ∀ ⦃x : α⦄, x sourceinvFun (toFun x) = x
  • The proposition that invFun is a local right-inverse of toFun on target.

    right_inv' : ∀ ⦃x : β⦄, x targettoFun (invFun x) = x

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.

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

    The inverse of a local equiv

    Equations
    • One or more equations did not get rendered due to their size.
    instance LocalEquiv.instCoeFunLocalEquivForAll {α : Type u_1} {β : Type u_2} :
    CoeFun (LocalEquiv α β) fun x => αβ
    Equations
    • LocalEquiv.instCoeFunLocalEquivForAll = { coe := LocalEquiv.toFun }
    def LocalEquiv.Simps.symm_apply {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    βα

    See Note [custom simps projection]

    Equations
    @[simp]
    theorem LocalEquiv.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) :
    (LocalEquiv.symm { toFun := f, invFun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il, right_inv' := ir }).toFun = g
    @[simp]
    theorem LocalEquiv.invFun_as_coe {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    e.invFun = (LocalEquiv.symm e).toFun
    @[simp]
    theorem LocalEquiv.map_source {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) {x : α} (h : x e.source) :
    LocalEquiv.toFun e x e.target
    @[simp]
    theorem LocalEquiv.map_target {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {x : β} (h : x e.target) :
    @[simp]
    theorem LocalEquiv.left_inv {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) {x : α} (h : x e.source) :
    @[simp]
    theorem LocalEquiv.right_inv {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {x : β} (h : x e.target) :
    theorem LocalEquiv.eq_symm_apply {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) {x : α} {y : β} (hx : x e.source) (hy : y e.target) :
    theorem LocalEquiv.mapsTo {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    Set.MapsTo e.toFun e.source e.target
    theorem LocalEquiv.symm_mapsTo {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) :
    Set.MapsTo (LocalEquiv.symm e).toFun e.target e.source
    theorem LocalEquiv.leftInvOn {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    Set.LeftInvOn (LocalEquiv.symm e).toFun e.toFun e.source
    theorem LocalEquiv.rightInvOn {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    Set.RightInvOn (LocalEquiv.symm e).toFun e.toFun e.target
    theorem LocalEquiv.invOn {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    Set.InvOn (LocalEquiv.symm e).toFun e.toFun e.source e.target
    theorem LocalEquiv.injOn {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    Set.InjOn e.toFun e.source
    theorem LocalEquiv.bijOn {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    Set.BijOn e.toFun e.source e.target
    theorem LocalEquiv.surjOn {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    Set.SurjOn e.toFun e.source e.target
    @[simp]
    theorem Equiv.toLocalEquiv_symm_apply {α : Type u_1} {β : Type u_2} (e : α β) :
    @[simp]
    theorem Equiv.toLocalEquiv_target {α : Type u_1} {β : Type u_2} (e : α β) :
    (Equiv.toLocalEquiv e).target = Set.univ
    @[simp]
    theorem Equiv.toLocalEquiv_source {α : Type u_1} {β : Type u_2} (e : α β) :
    (Equiv.toLocalEquiv e).source = Set.univ
    @[simp]
    theorem Equiv.toLocalEquiv_apply {α : Type u_1} {β : Type u_2} (e : α β) :
    (Equiv.toLocalEquiv e).toFun = e
    def Equiv.toLocalEquiv {α : Type u_1} {β : Type u_2} (e : α β) :

    Associate a LocalEquiv to an Equiv.

    Equations
    • One or more equations did not get rendered due to their size.
    instance LocalEquiv.inhabitedOfEmpty {α : Type u_1} {β : Type u_2} [inst : IsEmpty α] [inst : IsEmpty β] :
    Equations
    @[simp]
    theorem LocalEquiv.copy_apply {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : αβ) (hf : e.toFun = f) (g : βα) (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
    (LocalEquiv.copy e f hf g hg s hs t ht).toFun = f
    @[simp]
    theorem LocalEquiv.copy_symm_apply {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : αβ) (hf : e.toFun = f) (g : βα) (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
    (LocalEquiv.symm (LocalEquiv.copy e f hf g hg s hs t ht)).toFun = g
    @[simp]
    theorem LocalEquiv.copy_target {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : αβ) (hf : e.toFun = f) (g : βα) (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
    (LocalEquiv.copy e f hf g hg s hs t ht).target = t
    @[simp]
    theorem LocalEquiv.copy_source {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : αβ) (hf : e.toFun = f) (g : βα) (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
    (LocalEquiv.copy e f hf g hg s hs t ht).source = s
    def LocalEquiv.copy {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : αβ) (hf : e.toFun = f) (g : βα) (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :

    Create a copy of a LocalEquiv providing better definitional equalities.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem LocalEquiv.copy_eq {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : αβ) (hf : e.toFun = f) (g : βα) (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t) :
    LocalEquiv.copy e f hf g hg s hs t ht = e
    def LocalEquiv.toEquiv {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    e.source e.target

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

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem LocalEquiv.symm_source {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) :
    (LocalEquiv.symm e).source = e.target
    @[simp]
    theorem LocalEquiv.symm_target {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    (LocalEquiv.symm e).target = e.source
    @[simp]
    theorem LocalEquiv.symm_symm {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    theorem LocalEquiv.image_source_eq_target {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) :
    e.toFun '' e.source = e.target
    theorem LocalEquiv.forall_mem_target {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {p : βProp} :
    ((y : β) → y e.targetp y) (x : α) → x e.sourcep (LocalEquiv.toFun e x)
    theorem LocalEquiv.exists_mem_target {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {p : βProp} :
    (y, y e.target p y) x, x e.source p (LocalEquiv.toFun e x)
    def LocalEquiv.IsImage {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (s : Set α) (t : Set β) :

    We say that t : Set β is an image of s : Set α under a local equivalence if any of the following equivalent conditions hold:

    • e '' (e.source ∩ s) = e.target ∩ t∩ s) = e.target ∩ t∩ t;
    • e.source ∩ e ⁻¹ t = e.source ∩ s∩ e ⁻¹ t = e.source ∩ s⁻¹ t = e.source ∩ s∩ s;
    • ∀ x ∈ e.source, e x ∈ t ↔ x ∈ s∀ x ∈ e.source, e x ∈ t ↔ x ∈ s∈ e.source, e x ∈ t ↔ x ∈ s∈ t ↔ x ∈ s↔ x ∈ s∈ s (this one is used in the definition).
    Equations
    theorem LocalEquiv.IsImage.apply_mem_iff {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {x : α} (h : LocalEquiv.IsImage e s t) (hx : x e.source) :
    theorem LocalEquiv.IsImage.symm_apply_mem_iff {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) ⦃y : β :
    y e.target → (LocalEquiv.toFun (LocalEquiv.symm e) y s y t)
    theorem LocalEquiv.IsImage.symm {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :
    @[simp]
    theorem LocalEquiv.IsImage.symm_iff {α : Type u_2} {β : Type u_1} {e : LocalEquiv α β} {s : Set α} {t : Set β} :
    theorem LocalEquiv.IsImage.mapsTo {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :
    Set.MapsTo e.toFun (e.source s) (e.target t)
    theorem LocalEquiv.IsImage.symm_mapsTo {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :
    Set.MapsTo (LocalEquiv.symm e).toFun (e.target t) (e.source s)
    @[simp]
    theorem LocalEquiv.IsImage.restr_target {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :
    (LocalEquiv.IsImage.restr h).target = e.target t
    @[simp]
    theorem LocalEquiv.IsImage.restr_apply {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :
    (LocalEquiv.IsImage.restr h).toFun = e.toFun
    @[simp]
    theorem LocalEquiv.IsImage.restr_source {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :
    (LocalEquiv.IsImage.restr h).source = e.source s
    @[simp]
    theorem LocalEquiv.IsImage.restr_symm_apply {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :
    def LocalEquiv.IsImage.restr {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :

    Restrict a LocalEquiv to a pair of corresponding sets.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem LocalEquiv.IsImage.image_eq {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :
    e.toFun '' (e.source s) = e.target t
    theorem LocalEquiv.IsImage.symm_image_eq {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :
    (LocalEquiv.symm e).toFun '' (e.target t) = e.source s
    theorem LocalEquiv.IsImage.iff_preimage_eq {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} :
    LocalEquiv.IsImage e s t e.source e.toFun ⁻¹' t = e.source s
    theorem LocalEquiv.IsImage.preimage_eq {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} :
    LocalEquiv.IsImage e s te.source e.toFun ⁻¹' t = e.source s

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

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

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

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

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

    theorem LocalEquiv.IsImage.of_symm_preimage_eq {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} :
    e.target (LocalEquiv.symm e).toFun ⁻¹' s = e.target tLocalEquiv.IsImage e s t

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

    theorem LocalEquiv.IsImage.of_image_eq {α : Type u_2} {β : Type u_1} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : e.toFun '' (e.source s) = e.target t) :
    theorem LocalEquiv.IsImage.of_symm_image_eq {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : (LocalEquiv.symm e).toFun '' (e.target t) = e.source s) :
    theorem LocalEquiv.IsImage.compl {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : LocalEquiv.IsImage e s t) :
    theorem LocalEquiv.IsImage.inter {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β} (h : LocalEquiv.IsImage e s t) (h' : LocalEquiv.IsImage e s' t') :
    LocalEquiv.IsImage e (s s') (t t')
    theorem LocalEquiv.IsImage.union {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β} (h : LocalEquiv.IsImage e s t) (h' : LocalEquiv.IsImage e s' t') :
    LocalEquiv.IsImage e (s s') (t t')
    theorem LocalEquiv.IsImage.diff {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β} (h : LocalEquiv.IsImage e s t) (h' : LocalEquiv.IsImage e s' t') :
    LocalEquiv.IsImage e (s \ s') (t \ t')
    theorem LocalEquiv.IsImage.leftInvOn_piecewise {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {e' : LocalEquiv α β} [inst : (i : α) → Decidable (i s)] [inst : (i : β) → Decidable (i t)] (h : LocalEquiv.IsImage e s t) (h' : LocalEquiv.IsImage e' s t) :
    Set.LeftInvOn (Set.piecewise t (LocalEquiv.symm e).toFun (LocalEquiv.symm e').toFun) (Set.piecewise s e.toFun e'.toFun) (Set.ite s e.source e'.source)
    theorem LocalEquiv.IsImage.inter_eq_of_inter_eq_of_eqOn {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {e' : LocalEquiv α β} (h : LocalEquiv.IsImage e s t) (h' : LocalEquiv.IsImage e' s t) (hs : e.source s = e'.source s) (heq : Set.EqOn e.toFun e'.toFun (e.source s)) :
    e.target t = e'.target t
    theorem LocalEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {e' : LocalEquiv α β} (h : LocalEquiv.IsImage e s t) (hs : e.source s = e'.source s) (heq : Set.EqOn e.toFun e'.toFun (e.source s)) :
    Set.EqOn (LocalEquiv.symm e).toFun (LocalEquiv.symm e').toFun (e.target t)
    theorem LocalEquiv.isImage_source_target {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    LocalEquiv.IsImage e e.source e.target
    theorem LocalEquiv.isImage_source_target_of_disjoint {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) :
    LocalEquiv.IsImage e e'.source e'.target
    theorem LocalEquiv.image_source_inter_eq' {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (s : Set α) :
    e.toFun '' (e.source s) = e.target (LocalEquiv.symm e).toFun ⁻¹' s
    theorem LocalEquiv.image_source_inter_eq {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (s : Set α) :
    e.toFun '' (e.source s) = e.target (LocalEquiv.symm e).toFun ⁻¹' (e.source s)
    theorem LocalEquiv.image_eq_target_inter_inv_preimage {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) {s : Set α} (h : s e.source) :
    e.toFun '' s = e.target (LocalEquiv.symm e).toFun ⁻¹' s
    theorem LocalEquiv.symm_image_eq_source_inter_preimage {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {s : Set β} (h : s e.target) :
    (LocalEquiv.symm e).toFun '' s = e.source e.toFun ⁻¹' s
    theorem LocalEquiv.symm_image_target_inter_eq {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) (s : Set β) :
    (LocalEquiv.symm e).toFun '' (e.target s) = e.source e.toFun ⁻¹' (e.target s)
    theorem LocalEquiv.symm_image_target_inter_eq' {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) (s : Set β) :
    (LocalEquiv.symm e).toFun '' (e.target s) = e.source e.toFun ⁻¹' s
    theorem LocalEquiv.source_inter_preimage_inv_preimage {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (s : Set α) :
    e.source e.toFun ⁻¹' ((LocalEquiv.symm e).toFun ⁻¹' s) = e.source s
    theorem LocalEquiv.source_inter_preimage_target_inter {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) (s : Set β) :
    e.source e.toFun ⁻¹' (e.target s) = e.source e.toFun ⁻¹' s
    theorem LocalEquiv.target_inter_inv_preimage_preimage {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) (s : Set β) :
    e.target (LocalEquiv.symm e).toFun ⁻¹' (e.toFun ⁻¹' s) = e.target s
    theorem LocalEquiv.symm_image_image_of_subset_source {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) {s : Set α} (h : s e.source) :
    (LocalEquiv.symm e).toFun '' (e.toFun '' s) = s
    theorem LocalEquiv.image_symm_image_of_subset_target {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {s : Set β} (h : s e.target) :
    e.toFun '' ((LocalEquiv.symm e).toFun '' s) = s
    theorem LocalEquiv.source_subset_preimage_target {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    e.source e.toFun ⁻¹' e.target
    theorem LocalEquiv.symm_image_target_eq_source {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    (LocalEquiv.symm e).toFun '' e.target = e.source
    theorem LocalEquiv.target_subset_preimage_source {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) :
    e.target (LocalEquiv.symm e).toFun ⁻¹' e.source
    theorem LocalEquiv.ext {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {e' : LocalEquiv α β} (h : ∀ (x : α), LocalEquiv.toFun e x = LocalEquiv.toFun e' x) (hsymm : ∀ (x : β), LocalEquiv.toFun (LocalEquiv.symm e) x = LocalEquiv.toFun (LocalEquiv.symm e') x) (hs : e.source = e'.source) :
    e = e'

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

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

    Restricting a local equivalence to e.source ∩ s

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

    The identity local equiv

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

    The identity local equiv on a set s

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem LocalEquiv.ofSet_source {α : Type u_1} (s : Set α) :
    (LocalEquiv.ofSet s).source = s
    @[simp]
    theorem LocalEquiv.ofSet_target {α : Type u_1} (s : Set α) :
    (LocalEquiv.ofSet s).target = s
    @[simp]
    theorem LocalEquiv.ofSet_coe {α : Type u_1} (s : Set α) :
    (LocalEquiv.ofSet s).toFun = id
    def LocalEquiv.trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : LocalEquiv α β) (e' : LocalEquiv β γ) (h : e.target = e'.source) :

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

    Equations
    • One or more equations did not get rendered due to their size.
    def LocalEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :

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

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem LocalEquiv.coe_trans {α : Type u_1} {β : Type u_3} {γ : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :
    (LocalEquiv.trans e e').toFun = e'.toFun e.toFun
    @[simp]
    theorem LocalEquiv.coe_trans_symm {α : Type u_1} {β : Type u_3} {γ : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :
    theorem LocalEquiv.trans_apply {α : Type u_2} {β : Type u_3} {γ : Type u_1} (e : LocalEquiv α β) (e' : LocalEquiv β γ) {x : α} :
    @[simp]
    theorem LocalEquiv.trans_source {α : Type u_1} {β : Type u_3} {γ : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :
    (LocalEquiv.trans e e').source = e.source e.toFun ⁻¹' e'.source
    theorem LocalEquiv.trans_source' {α : Type u_1} {β : Type u_3} {γ : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :
    (LocalEquiv.trans e e').source = e.source e.toFun ⁻¹' (e.target e'.source)
    theorem LocalEquiv.trans_source'' {α : Type u_1} {β : Type u_3} {γ : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :
    (LocalEquiv.trans e e').source = (LocalEquiv.symm e).toFun '' (e.target e'.source)
    theorem LocalEquiv.image_trans_source {α : Type u_2} {β : Type u_1} {γ : Type u_3} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :
    e.toFun '' (LocalEquiv.trans e e').source = e.target e'.source
    @[simp]
    theorem LocalEquiv.trans_target {α : Type u_2} {β : Type u_3} {γ : Type u_1} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :
    (LocalEquiv.trans e e').target = e'.target (LocalEquiv.symm e').toFun ⁻¹' e.target
    theorem LocalEquiv.trans_target' {α : Type u_2} {β : Type u_3} {γ : Type u_1} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :
    (LocalEquiv.trans e e').target = e'.target (LocalEquiv.symm e').toFun ⁻¹' (e'.source e.target)
    theorem LocalEquiv.trans_target'' {α : Type u_2} {β : Type u_3} {γ : Type u_1} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :
    (LocalEquiv.trans e e').target = e'.toFun '' (e'.source e.target)
    theorem LocalEquiv.inv_image_trans_target {α : Type u_3} {β : Type u_1} {γ : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv β γ) :
    (LocalEquiv.symm e').toFun '' (LocalEquiv.trans e e').target = e'.source e.target
    theorem LocalEquiv.trans_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_1} {δ : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv β γ) (e'' : LocalEquiv γ δ) :
    @[simp]
    theorem LocalEquiv.trans_refl {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    @[simp]
    theorem LocalEquiv.refl_trans {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :
    theorem LocalEquiv.trans_ofSet {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) (s : Set β) :
    theorem LocalEquiv.trans_refl_restr {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) (s : Set β) :
    theorem LocalEquiv.trans_refl_restr' {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) (s : Set β) :
    theorem LocalEquiv.restr_trans {α : Type u_1} {β : Type u_3} {γ : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv β γ) (s : Set α) :
    theorem LocalEquiv.mem_symm_trans_source {α : Type u_1} {β : Type u_3} {γ : Type u_2} (e : LocalEquiv α β) {e' : LocalEquiv α γ} {x : α} (he : x e.source) (he' : x e'.source) :

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

    @[simp]
    theorem LocalEquiv.transEquiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : LocalEquiv α β) (e' : β γ) :
    @[simp]
    theorem LocalEquiv.transEquiv_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : LocalEquiv α β) (e' : β γ) :
    (LocalEquiv.transEquiv e e').source = e.source
    @[simp]
    theorem LocalEquiv.transEquiv_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : LocalEquiv α β) (e' : β γ) :
    (LocalEquiv.transEquiv e e').target = ↑(Equiv.symm e') ⁻¹' e.target
    @[simp]
    theorem LocalEquiv.transEquiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : LocalEquiv α β) (e' : β γ) :
    ∀ (a : α), LocalEquiv.toFun (LocalEquiv.transEquiv e e') a = e' (LocalEquiv.toFun e a)
    def LocalEquiv.transEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : LocalEquiv α β) (e' : β γ) :

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

    Equations
    • One or more equations did not get rendered due to their size.
    theorem LocalEquiv.transEquiv_eq_trans {α : Type u_3} {β : Type u_1} {γ : Type u_2} (e : LocalEquiv α β) (e' : β γ) :
    @[simp]
    theorem Equiv.transLocalEquiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : LocalEquiv β γ) (e : α β) :
    ∀ (a : α), LocalEquiv.toFun (Equiv.transLocalEquiv e' e) a = LocalEquiv.toFun e' (e a)
    @[simp]
    theorem Equiv.transLocalEquiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : LocalEquiv β γ) (e : α β) :
    @[simp]
    theorem Equiv.transLocalEquiv_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : LocalEquiv β γ) (e : α β) :
    (Equiv.transLocalEquiv e' e).source = e ⁻¹' e'.source
    @[simp]
    theorem Equiv.transLocalEquiv_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : LocalEquiv β γ) (e : α β) :
    (Equiv.transLocalEquiv e' e).target = e'.target
    def Equiv.transLocalEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : LocalEquiv β γ) (e : α β) :

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

    Equations
    • One or more equations did not get rendered due to their size.
    theorem Equiv.transLocalEquiv_eq_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : LocalEquiv β γ) (e : α β) :
    def LocalEquiv.EqOnSource {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv α β) :

    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 local equiv.

    Equations
    instance LocalEquiv.eqOnSourceSetoid {α : Type u_1} {β : Type u_2} :

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

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

    Two equivalent local equivs have the same source

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

    Two equivalent local equivs coincide on the source

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

    Two equivalent local equivs have the same target

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

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

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

    Two equivalent local equivs have coinciding inverses on the target

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

    Composition of local equivs respects equivalence

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

    Restriction of local equivs respects equivalence

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

    Preimages are respected by equivalence

    theorem LocalEquiv.trans_self_symm {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) :

    Composition of a local equiv and its inverse is equivalent to the restriction of the identity to the source

    theorem LocalEquiv.trans_symm_self {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) :

    Composition of the inverse of a local equiv and this local equiv is equivalent to the restriction of the identity to the target

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

    Two equivalent local equivs are equal when the source and target are univ

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

    The product of two local equivs, as a local equiv on the product.

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

    Combine two LocalEquivs using Set.piecewise. The source of the new LocalEquiv is s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s∩ s ∪ e'.source \ s∪ e'.source \ s, and similarly for target. The function sends e.source ∩ s∩ s to e.target ∩ t∩ 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.
    theorem LocalEquiv.symm_piecewise {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv α β) {s : Set α} {t : Set β} [inst : (x : α) → Decidable (x s)] [inst : (y : β) → Decidable (y t)] (H : LocalEquiv.IsImage e s t) (H' : LocalEquiv.IsImage e' s t) :
    @[simp]
    theorem LocalEquiv.disjointUnion_target {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [inst : (x : α) → Decidable (x e.source)] [inst : (y : β) → Decidable (y e.target)] :
    (LocalEquiv.disjointUnion e e' hs ht).target = e.target e'.target
    @[simp]
    theorem LocalEquiv.disjointUnion_source {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [inst : (x : α) → Decidable (x e.source)] [inst : (y : β) → Decidable (y e.target)] :
    (LocalEquiv.disjointUnion e e' hs ht).source = e.source e'.source
    @[simp]
    theorem LocalEquiv.disjointUnion_symm_apply {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [inst : (x : α) → Decidable (x e.source)] [inst : (y : β) → Decidable (y e.target)] :
    (LocalEquiv.symm (LocalEquiv.disjointUnion e e' hs ht)).toFun = Set.piecewise e.target (LocalEquiv.symm e).toFun (LocalEquiv.symm e').toFun
    @[simp]
    theorem LocalEquiv.disjointUnion_apply {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [inst : (x : α) → Decidable (x e.source)] [inst : (y : β) → Decidable (y e.target)] :
    (LocalEquiv.disjointUnion e e' hs ht).toFun = Set.piecewise e.source e.toFun e'.toFun
    def LocalEquiv.disjointUnion {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (e' : LocalEquiv α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) [inst : (x : α) → Decidable (x e.source)] [inst : (y : β) → Decidable (y e.target)] :

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

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

    The product of a family of local equivs, as a local equiv on the pi type.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Set.BijOn.toLocalEquiv_apply {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : αβ) (s : Set α) (t : Set β) (hf : Set.BijOn f s t) :
    (Set.BijOn.toLocalEquiv f s t hf).toFun = f
    @[simp]
    theorem Set.BijOn.toLocalEquiv_target {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : αβ) (s : Set α) (t : Set β) (hf : Set.BijOn f s t) :
    (Set.BijOn.toLocalEquiv f s t hf).target = t
    @[simp]
    theorem Set.BijOn.toLocalEquiv_symm_apply {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : αβ) (s : Set α) (t : Set β) (hf : Set.BijOn f s t) :
    @[simp]
    theorem Set.BijOn.toLocalEquiv_source {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : αβ) (s : Set α) (t : Set β) (hf : Set.BijOn f s t) :
    (Set.BijOn.toLocalEquiv f s t hf).source = s
    noncomputable def Set.BijOn.toLocalEquiv {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : αβ) (s : Set α) (t : Set β) (hf : Set.BijOn f s t) :

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

    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable def Set.InjOn.toLocalEquiv {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : αβ) (s : Set α) (hf : Set.InjOn f s) :

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

    Equations
    @[simp]
    theorem Equiv.trans_toLocalEquiv {α : Type u_1} {β : Type u_3} {γ : Type u_2} (e : α β) (e' : β γ) :