# mathlib3documentation

logic.equiv.local_equiv

# Local equivalences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This files defines equivalences between subsets of given types. An element `e` of `local_equiv α β` is made of two maps `e.to_fun` and `e.inv_fun` 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.to_fun x` and `e.inv_fun y`.

## Main definitions #

`equiv.to_local_equiv`: associating a local equiv to an equiv, with source = target = univ `local_equiv.symm` : the inverse of a local equiv `local_equiv.trans` : the composition of two local equivs `local_equiv.refl` : the identity local equiv `local_equiv.of_set` : the identity on a set `s` `eq_on_source` : 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:

• equivs on subtypes
• pairs of functions taking values in `option α` and `option β`, equal to none where the local equivalence is not defined
• pairs of functions defined everywhere, keeping the source and target as additional data

Each of these implementations has pros and cons.

• When dealing with subtypes, one still need to define additional API for composition and restriction of domains. Checking that one always belongs to the right subtype makes things very tedious, and leads quickly to DTT hell (as the subtype `u ∩ v` is not the "same" as `v ∩ u`, for instance).
• With option-valued functions, the composition is very neat (it is just the usual composition, and the domain is restricted automatically). These are implemented in `pequiv.lean`. For manifolds, where one wants to discuss thoroughly the smoothness of the maps, this creates however a lot of overhead as one would need to extend all classes of smoothness to option-valued maps.
• The local_equiv version as explained above is easier to use for manifolds. The drawback is that there is extra useless data (the values of `to_fun` and `inv_fun` outside of `source` and `target`). In particular, the equality notion between local equivs is not "the right one", i.e., coinciding source and target and equality there. Moreover, there are no local equivs in this sense between an empty type and a nonempty type. Since empty types are not that useful, and since one almost never needs to talk about equal local equivs, this is not an issue in practice. Still, we introduce an equivalence relation `eq_on_source` that captures this right notion of equality, and show that many properties are invariant under this equivalence relation.

### Local coding conventions #

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

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

Equations

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

structure local_equiv (α : 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 `to_fun : α → β` and `inv_fun : β → α` map `source` to `target` and conversely, and are inverse to each other there. The values of `to_fun` outside of `source` and of `inv_fun` outside of `target` are irrelevant.

Instances for `local_equiv`
@[protected, instance]
def local_equiv.inhabited {α : Type u_1} {β : Type u_2} [inhabited α] [inhabited β] :
Equations
@[protected]
def local_equiv.symm {α : Type u_1} {β : Type u_2} (e : β) :
α

The inverse of a local equiv

Equations
@[protected, instance]
def local_equiv.has_coe_to_fun {α : Type u_1} {β : Type u_2} :
(λ (_x : β), α β)
Equations
def local_equiv.simps.symm_apply {α : Type u_1} {β : Type u_2} (e : β) :
β α
Equations
@[simp]
theorem local_equiv.coe_mk {α : Type u_1} {β : Type u_2} (f : α β) (g : β α) (s : set α) (t : set β) (ml : ⦃x : α⦄, x s f x t) (mr : ⦃x : β⦄, x t g x s) (il : ⦃x : α⦄, x s g (f x) = x) (ir : ⦃x : β⦄, x t f (g x) = x) :
{to_fun := f, inv_fun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il, right_inv' := ir} = f
@[simp]
theorem local_equiv.coe_symm_mk {α : Type u_1} {β : Type u_2} (f : α β) (g : β α) (s : set α) (t : set β) (ml : ⦃x : α⦄, x s f x t) (mr : ⦃x : β⦄, x t g x s) (il : ⦃x : α⦄, x s g (f x) = x) (ir : ⦃x : β⦄, x t f (g x) = x) :
({to_fun := f, inv_fun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il, right_inv' := ir}.symm) = g
@[simp]
theorem local_equiv.to_fun_as_coe {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem local_equiv.inv_fun_as_coe {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem local_equiv.map_source {α : Type u_1} {β : Type u_2} (e : β) {x : α} (h : x e.source) :
@[simp]
theorem local_equiv.map_target {α : Type u_1} {β : Type u_2} (e : β) {x : β} (h : x e.target) :
@[simp]
theorem local_equiv.left_inv {α : Type u_1} {β : Type u_2} (e : β) {x : α} (h : x e.source) :
(e.symm) (e x) = x
@[simp]
theorem local_equiv.right_inv {α : Type u_1} {β : Type u_2} (e : β) {x : β} (h : x e.target) :
e ((e.symm) x) = x
theorem local_equiv.eq_symm_apply {α : Type u_1} {β : Type u_2} (e : β) {x : α} {y : β} (hx : x e.source) (hy : y e.target) :
x = (e.symm) y e x = y
@[protected]
theorem local_equiv.maps_to {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_equiv.symm_maps_to {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_equiv.left_inv_on {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_equiv.right_inv_on {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_equiv.inv_on {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_equiv.inj_on {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_equiv.bij_on {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_equiv.surj_on {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem equiv.to_local_equiv_source {α : Type u_1} {β : Type u_2} (e : α β) :
@[simp]
theorem equiv.to_local_equiv_target {α : Type u_1} {β : Type u_2} (e : α β) :
@[simp]
theorem equiv.to_local_equiv_apply {α : Type u_1} {β : Type u_2} (e : α β) :
@[simp]
theorem equiv.to_local_equiv_symm_apply {α : Type u_1} {β : Type u_2} (e : α β) :
def equiv.to_local_equiv {α : Type u_1} {β : Type u_2} (e : α β) :
β

Associating a local_equiv to an equiv

Equations
@[protected, instance]
def local_equiv.inhabited_of_empty {α : Type u_1} {β : Type u_2} [is_empty α] [is_empty β] :
Equations
@[simp]
theorem local_equiv.copy_apply {α : Type u_1} {β : Type u_2} (e : β) (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 local_equiv.copy_target {α : Type u_1} {β : Type u_2} (e : β) (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 local_equiv.copy_symm_apply {α : Type u_1} {β : Type u_2} (e : β) (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
@[simp]
theorem local_equiv.copy_source {α : Type u_1} {β : Type u_2} (e : β) (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
def local_equiv.copy {α : Type u_1} {β : Type u_2} (e : β) (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 `local_equiv` providing better definitional equalities.

Equations
theorem local_equiv.copy_eq {α : Type u_1} {β : Type u_2} (e : β) (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
@[protected]
def local_equiv.to_equiv {α : Type u_1} {β : Type u_2} (e : β) :

Associating to a local_equiv an equiv between the source and the target

Equations
@[simp]
theorem local_equiv.symm_source {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem local_equiv.symm_target {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem local_equiv.symm_symm {α : Type u_1} {β : Type u_2} (e : β) :
e.symm.symm = e
theorem local_equiv.image_source_eq_target {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_equiv.forall_mem_target {α : Type u_1} {β : Type u_2} (e : β) {p : β Prop} :
( (y : β), y e.target p y) (x : α), x e.source p (e x)
theorem local_equiv.exists_mem_target {α : Type u_1} {β : Type u_2} (e : β) {p : β Prop} :
( (y : β) (H : y e.target), p y) (x : α) (H : x e.source), p (e x)
def local_equiv.is_image {α : Type u_1} {β : Type u_2} (e : β) (s : set α) (t : set β) :
Prop

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`;
• `e.source ∩ e ⁻¹ t = e.source ∩ s`;
• `∀ x ∈ e.source, e x ∈ t ↔ x ∈ s` (this one is used in the definition).
Equations
theorem local_equiv.is_image.apply_mem_iff {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} {x : α} (h : e.is_image s t) (hx : x e.source) :
e x t x s
theorem local_equiv.is_image.symm_apply_mem_iff {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) ⦃y : β⦄ :
y e.target ((e.symm) y s y t)
@[protected]
theorem local_equiv.is_image.symm {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
@[simp]
theorem local_equiv.is_image.symm_iff {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :
@[protected]
theorem local_equiv.is_image.maps_to {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
(e.source s) (e.target t)
theorem local_equiv.is_image.symm_maps_to {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
@[simp]
theorem local_equiv.is_image.restr_source {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
@[simp]
theorem local_equiv.is_image.restr_target {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
@[simp]
theorem local_equiv.is_image.restr_symm_apply {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
def local_equiv.is_image.restr {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
β

Restrict a `local_equiv` to a pair of corresponding sets.

Equations
@[simp]
theorem local_equiv.is_image.restr_apply {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_equiv.is_image.image_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
e '' (e.source s) = e.target t
theorem local_equiv.is_image.symm_image_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
(e.symm) '' (e.target t) = e.source s
theorem local_equiv.is_image.iff_preimage_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :
theorem local_equiv.is_image.preimage_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :

Alias of the forward direction of `local_equiv.is_image.iff_preimage_eq`.

theorem local_equiv.is_image.of_preimage_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :

Alias of the reverse direction of `local_equiv.is_image.iff_preimage_eq`.

theorem local_equiv.is_image.iff_symm_preimage_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :
theorem local_equiv.is_image.symm_preimage_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :

Alias of the forward direction of `local_equiv.is_image.iff_symm_preimage_eq`.

theorem local_equiv.is_image.of_symm_preimage_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :

Alias of the reverse direction of `local_equiv.is_image.iff_symm_preimage_eq`.

theorem local_equiv.is_image.of_image_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e '' (e.source s) = e.target t) :
e.is_image s t
theorem local_equiv.is_image.of_symm_image_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : (e.symm) '' (e.target t) = e.source s) :
e.is_image s t
@[protected]
theorem local_equiv.is_image.compl {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
@[protected]
theorem local_equiv.is_image.inter {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} {s' : set α} {t' : set β} (h : e.is_image s t) (h' : e.is_image s' t') :
e.is_image (s s') (t t')
@[protected]
theorem local_equiv.is_image.union {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} {s' : set α} {t' : set β} (h : e.is_image s t) (h' : e.is_image s' t') :
e.is_image (s s') (t t')
@[protected]
theorem local_equiv.is_image.diff {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} {s' : set α} {t' : set β} (h : e.is_image s t) (h' : e.is_image s' t') :
e.is_image (s \ s') (t \ t')
theorem local_equiv.is_image.left_inv_on_piecewise {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} {e' : β} [Π (i : α), decidable (i s)] [Π (i : β), decidable (i t)] (h : e.is_image s t) (h' : e'.is_image s t) :
theorem local_equiv.is_image.inter_eq_of_inter_eq_of_eq_on {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} {e' : β} (h : e.is_image s t) (h' : e'.is_image s t) (hs : e.source s = e'.source s) (Heq : e' (e.source s)) :
e.target t = e'.target t
theorem local_equiv.is_image.symm_eq_on_of_inter_eq_of_eq_on {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} {e' : β} (h : e.is_image s t) (hs : e.source s = e'.source s) (Heq : e' (e.source s)) :
theorem local_equiv.is_image_source_target {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_equiv.is_image_source_target_of_disjoint {α : Type u_1} {β : Type u_2} (e e' : β) (hs : e'.source) (ht : e'.target) :
theorem local_equiv.image_source_inter_eq' {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
theorem local_equiv.image_source_inter_eq {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
theorem local_equiv.image_eq_target_inter_inv_preimage {α : Type u_1} {β : Type u_2} (e : β) {s : set α} (h : s e.source) :
theorem local_equiv.symm_image_eq_source_inter_preimage {α : Type u_1} {β : Type u_2} (e : β) {s : set β} (h : s e.target) :
theorem local_equiv.symm_image_target_inter_eq {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :
theorem local_equiv.symm_image_target_inter_eq' {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :
theorem local_equiv.source_inter_preimage_inv_preimage {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
theorem local_equiv.source_inter_preimage_target_inter {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :
theorem local_equiv.target_inter_inv_preimage_preimage {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :
theorem local_equiv.symm_image_image_of_subset_source {α : Type u_1} {β : Type u_2} (e : β) {s : set α} (h : s e.source) :
(e.symm) '' (e '' s) = s
theorem local_equiv.image_symm_image_of_subset_target {α : Type u_1} {β : Type u_2} (e : β) {s : set β} (h : s e.target) :
e '' ((e.symm) '' s) = s
theorem local_equiv.source_subset_preimage_target {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_equiv.symm_image_target_eq_source {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_equiv.target_subset_preimage_source {α : Type u_1} {β : Type u_2} (e : β) :
@[protected, ext]
theorem local_equiv.ext {α : Type u_1} {β : Type u_2} {e e' : β} (h : (x : α), e x = e' x) (hsymm : (x : β), (e.symm) x = (e'.symm) x) (hs : e.source = e'.source) :
e = e'

Two local equivs that have the same `source`, same `to_fun` and same `inv_fun`, coincide.

@[protected]
def local_equiv.restr {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
β

Restricting a local equivalence to e.source ∩ s

Equations
@[simp]
theorem local_equiv.restr_coe {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
(e.restr s) = e
@[simp]
theorem local_equiv.restr_coe_symm {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
((e.restr s).symm) = (e.symm)
@[simp]
theorem local_equiv.restr_source {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
(e.restr s).source = e.source s
@[simp]
theorem local_equiv.restr_target {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
theorem local_equiv.restr_eq_of_source_subset {α : Type u_1} {β : Type u_2} {e : β} {s : set α} (h : e.source s) :
e.restr s = e
@[simp]
theorem local_equiv.restr_univ {α : Type u_1} {β : Type u_2} {e : β} :
= e
@[protected]
def local_equiv.refl (α : Type u_1) :
α

The identity local equiv

Equations
@[simp]
theorem local_equiv.refl_source {α : Type u_1} :
@[simp]
theorem local_equiv.refl_target {α : Type u_1} :
@[simp]
theorem local_equiv.refl_coe {α : Type u_1} :
@[simp]
theorem local_equiv.refl_symm {α : Type u_1} :
@[simp]
theorem local_equiv.refl_restr_source {α : Type u_1} (s : set α) :
@[simp]
theorem local_equiv.refl_restr_target {α : Type u_1} (s : set α) :
def local_equiv.of_set {α : Type u_1} (s : set α) :
α

The identity local equiv on a set `s`

Equations
@[simp]
theorem local_equiv.of_set_source {α : Type u_1} (s : set α) :
@[simp]
theorem local_equiv.of_set_target {α : Type u_1} (s : set α) :
@[simp]
theorem local_equiv.of_set_coe {α : Type u_1} (s : set α) :
@[simp]
theorem local_equiv.of_set_symm {α : Type u_1} (s : set α) :
@[protected]
def local_equiv.trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) (h : e.target = e'.source) :
γ

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

Equations
@[protected]
def local_equiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
γ

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

Equations
@[simp]
theorem local_equiv.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
(e.trans e') = e' e
@[simp]
theorem local_equiv.coe_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
((e.trans e').symm) = (e.symm) (e'.symm)
theorem local_equiv.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) {x : α} :
(e.trans e') x = e' (e x)
theorem local_equiv.trans_symm_eq_symm_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
(e.trans e').symm = e'.symm.trans e.symm
@[simp]
theorem local_equiv.trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_equiv.trans_source' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_equiv.trans_source'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
(e.trans e').source = (e.symm) '' (e.target e'.source)
theorem local_equiv.image_trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
@[simp]
theorem local_equiv.trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_equiv.trans_target' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_equiv.trans_target'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
(e.trans e').target = e' '' (e'.source e.target)
theorem local_equiv.inv_image_trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
(e'.symm) '' (e.trans e').target = e'.source e.target
theorem local_equiv.trans_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : γ) (e'' : δ) :
(e.trans e').trans e'' = e.trans (e'.trans e'')
@[simp]
theorem local_equiv.trans_refl {α : Type u_1} {β : Type u_2} (e : β) :
e.trans = e
@[simp]
theorem local_equiv.refl_trans {α : Type u_1} {β : Type u_2} (e : β) :
e = e
theorem local_equiv.trans_refl_restr {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :
theorem local_equiv.trans_refl_restr' {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :
theorem local_equiv.restr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) (s : set α) :
(e.restr s).trans e' = (e.trans e').restr s
theorem local_equiv.mem_symm_trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) {e' : γ} {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.

@[simp]
theorem local_equiv.trans_equiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β γ) (ᾰ : α) :
(e.trans_equiv e') = e' (e ᾰ)
@[simp]
theorem local_equiv.trans_equiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β γ) (ᾰ : γ) :
((e.trans_equiv e').symm) = (e.symm) ((e'.symm) ᾰ)
@[simp]
theorem local_equiv.trans_equiv_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β γ) :
@[simp]
theorem local_equiv.trans_equiv_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β γ) :
def local_equiv.trans_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β γ) :
γ

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

Equations
theorem local_equiv.trans_equiv_eq_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β γ) :
@[simp]
theorem equiv.trans_local_equiv_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α β) :
@[simp]
theorem equiv.trans_local_equiv_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α β) (ᾰ : α) :
e) = e' (e ᾰ)
@[simp]
theorem equiv.trans_local_equiv_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α β) (ᾰ : γ) :
e).symm) = (e.symm) ((e'.symm) ᾰ)
@[simp]
theorem equiv.trans_local_equiv_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α β) :
e).target = e'.target
def equiv.trans_local_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α β) :
γ

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

Equations
theorem equiv.trans_local_equiv_eq_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α β) :
def local_equiv.eq_on_source {α : Type u_1} {β : Type u_2} (e e' : β) :
Prop

`eq_on_source 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
@[protected, instance]
def local_equiv.eq_on_source_setoid {α : Type u_1} {β : Type u_2} :
setoid β)

`eq_on_source` is an equivalence relation

Equations
theorem local_equiv.eq_on_source_refl {α : Type u_1} {β : Type u_2} (e : β) :
e e
theorem local_equiv.eq_on_source.source_eq {α : Type u_1} {β : Type u_2} {e e' : β} (h : e e') :

Two equivalent local equivs have the same source

theorem local_equiv.eq_on_source.eq_on {α : Type u_1} {β : Type u_2} {e e' : β} (h : e e') :
e' e.source

Two equivalent local equivs coincide on the source

theorem local_equiv.eq_on_source.target_eq {α : Type u_1} {β : Type u_2} {e e' : β} (h : e e') :

Two equivalent local equivs have the same target

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

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

theorem local_equiv.eq_on_source.symm_eq_on {α : Type u_1} {β : Type u_2} {e e' : β} (h : e e') :

Two equivalent local equivs have coinciding inverses on the target

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

Composition of local equivs respects equivalence

theorem local_equiv.eq_on_source.restr {α : Type u_1} {β : Type u_2} {e e' : β} (he : e e') (s : set α) :
e.restr s e'.restr s

Restriction of local equivs respects equivalence

theorem local_equiv.eq_on_source.source_inter_preimage_eq {α : Type u_1} {β : Type u_2} {e e' : β} (he : e e') (s : set β) :

Preimages are respected by equivalence

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

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

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

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

theorem local_equiv.eq_of_eq_on_source_univ {α : Type u_1} {β : Type u_2} (e e' : β) (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 local_equiv.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : δ) :
local_equiv × γ) × δ)

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

Equations
@[simp]
theorem local_equiv.prod_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : δ) :
@[simp]
theorem local_equiv.prod_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : δ) :
@[simp]
theorem local_equiv.prod_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : δ) :
(e.prod e') = λ (p : α × γ), (e p.fst, e' p.snd)
theorem local_equiv.prod_coe_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : δ) :
((e.prod e').symm) = λ (p : β × δ), ((e.symm) p.fst, (e'.symm) p.snd)
@[simp]
theorem local_equiv.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : δ) :
(e.prod e').symm = e.symm.prod e'.symm
@[simp]
theorem local_equiv.refl_prod_refl {α : Type u_1} {β : Type u_2} :
@[simp]
theorem local_equiv.prod_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {η : Type u_5} {ε : Type u_6} (e : β) (f : γ) (e' : η) (f' : ε) :
(e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
def local_equiv.piecewise {α : Type u_1} {β : Type u_2} (e e' : β) (s : set α) (t : set β) [Π (x : α), decidable (x s)] [Π (y : β), decidable (y t)] (H : e.is_image s t) (H' : e'.is_image s t) :
β

Combine two `local_equiv`s using `set.piecewise`. The source of the new `local_equiv` 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.is_image s t` and `e'.is_image s t`.

Equations
@[simp]
theorem local_equiv.piecewise_source {α : Type u_1} {β : Type u_2} (e e' : β) (s : set α) (t : set β) [Π (x : α), decidable (x s)] [Π (y : β), decidable (y t)] (H : e.is_image s t) (H' : e'.is_image s t) :
(e.piecewise e' s t H H').source = s.ite e.source e'.source
@[simp]
theorem local_equiv.piecewise_symm_apply {α : Type u_1} {β : Type u_2} (e e' : β) (s : set α) (t : set β) [Π (x : α), decidable (x s)] [Π (y : β), decidable (y t)] (H : e.is_image s t) (H' : e'.is_image s t) :
((e.piecewise e' s t H H').symm) = t.piecewise (e.symm) (e'.symm)
@[simp]
theorem local_equiv.piecewise_apply {α : Type u_1} {β : Type u_2} (e e' : β) (s : set α) (t : set β) [Π (x : α), decidable (x s)] [Π (y : β), decidable (y t)] (H : e.is_image s t) (H' : e'.is_image s t) :
(e.piecewise e' s t H H') = s.piecewise e e'
@[simp]
theorem local_equiv.piecewise_target {α : Type u_1} {β : Type u_2} (e e' : β) (s : set α) (t : set β) [Π (x : α), decidable (x s)] [Π (y : β), decidable (y t)] (H : e.is_image s t) (H' : e'.is_image s t) :
(e.piecewise e' s t H H').target = t.ite e.target e'.target
theorem local_equiv.symm_piecewise {α : Type u_1} {β : Type u_2} (e e' : β) {s : set α} {t : set β} [Π (x : α), decidable (x s)] [Π (y : β), decidable (y t)] (H : e.is_image s t) (H' : e'.is_image s t) :
(e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s _ _
@[simp]
theorem local_equiv.disjoint_union_source {α : Type u_1} {β : Type u_2} (e e' : β) (hs : e'.source) (ht : e'.target) [Π (x : α), decidable (x e.source)] [Π (y : β), decidable (y e.target)] :
def local_equiv.disjoint_union {α : Type u_1} {β : Type u_2} (e e' : β) (hs : e'.source) (ht : e'.target) [Π (x : α), decidable (x e.source)] [Π (y : β), decidable (y e.target)] :
β

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

Equations
@[simp]
theorem local_equiv.disjoint_union_symm_apply {α : Type u_1} {β : Type u_2} (e e' : β) (hs : e'.source) (ht : e'.target) [Π (x : α), decidable (x e.source)] [Π (y : β), decidable (y e.target)] :
@[simp]
theorem local_equiv.disjoint_union_target {α : Type u_1} {β : Type u_2} (e e' : β) (hs : e'.source) (ht : e'.target) [Π (x : α), decidable (x e.source)] [Π (y : β), decidable (y e.target)] :
@[simp]
theorem local_equiv.disjoint_union_apply {α : Type u_1} {β : Type u_2} (e e' : β) (hs : e'.source) (ht : e'.target) [Π (x : α), decidable (x e.source)] [Π (y : β), decidable (y e.target)] :
theorem local_equiv.disjoint_union_eq_piecewise {α : Type u_1} {β : Type u_2} (e e' : β) (hs : e'.source) (ht : e'.target) [Π (x : α), decidable (x e.source)] [Π (y : β), decidable (y e.target)] :
e.disjoint_union e' hs ht = e.piecewise e' e.source e.target _ _
@[protected]
def local_equiv.pi {ι : Type u_5} {αi : ι Type u_6} {βi : ι Type u_7} (ei : Π (i : ι), local_equiv (αi i) (βi i)) :
local_equiv (Π (i : ι), αi i) (Π (i : ι), βi i)

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

Equations
@[simp]
theorem local_equiv.pi_source {ι : Type u_5} {αi : ι Type u_6} {βi : ι Type u_7} (ei : Π (i : ι), local_equiv (αi i) (βi i)) :
(local_equiv.pi ei).source = set.univ.pi (λ (i : ι), (ei i).source)
@[simp]
theorem local_equiv.pi_symm_apply {ι : Type u_5} {αi : ι Type u_6} {βi : ι Type u_7} (ei : Π (i : ι), local_equiv (αi i) (βi i)) :
((local_equiv.pi ei).symm) = λ (f : Π (i : ι), βi i) (i : ι), ((ei i).symm) (f i)
@[simp]
theorem local_equiv.pi_target {ι : Type u_5} {αi : ι Type u_6} {βi : ι Type u_7} (ei : Π (i : ι), local_equiv (αi i) (βi i)) :
(local_equiv.pi ei).target = set.univ.pi (λ (i : ι), (ei i).target)
@[simp]
theorem local_equiv.pi_apply {ι : Type u_5} {αi : ι Type u_6} {βi : ι Type u_7} (ei : Π (i : ι), local_equiv (αi i) (βi i)) :
(local_equiv.pi ei) = λ (f : Π (i : ι), αi i) (i : ι), (ei i) (f i)
@[simp]
theorem set.bij_on.to_local_equiv_source {α : Type u_1} {β : Type u_2} [nonempty α] (f : α β) (s : set α) (t : set β) (hf : s t) :
hf).source = s
@[simp]
theorem set.bij_on.to_local_equiv_symm_apply {α : Type u_1} {β : Type u_2} [nonempty α] (f : α β) (s : set α) (t : set β) (hf : s t) :
t hf).symm) =
@[simp]
theorem set.bij_on.to_local_equiv_target {α : Type u_1} {β : Type u_2} [nonempty α] (f : α β) (s : set α) (t : set β) (hf : s t) :
hf).target = t
@[simp]
theorem set.bij_on.to_local_equiv_apply {α : Type u_1} {β : Type u_2} [nonempty α] (f : α β) (s : set α) (t : set β) (hf : s t) :
hf) = f
noncomputable def set.bij_on.to_local_equiv {α : Type u_1} {β : Type u_2} [nonempty α] (f : α β) (s : set α) (t : set β) (hf : s t) :
β

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

Equations
@[simp]
noncomputable def set.inj_on.to_local_equiv {α : Type u_1} {β : Type u_2} [nonempty α] (f : α β) (s : set α) (hf : s) :
β

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

Equations
@[simp]
theorem equiv.refl_to_local_equiv {α : Type u_1} :
@[simp]
theorem equiv.symm_to_local_equiv {α : Type u_1} {β : Type u_2} (e : α β) :
@[simp]
theorem equiv.trans_to_local_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (e' : β γ) :