mathlib3 documentation

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:

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 local_equiv, then it should use e.source ∩ s or e.target ∩ t, not s ∩ e.source or t ∩ e.target.

source
def mfld_cfg  :
simps_cfg

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

Equations
source
meta def tactic.interactive.mfld_set_tac  :
tactic unit

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

source
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
source
@[protected, instance]
def local_equiv.inhabited {α : Type u_1} {β : Type u_2} [inhabited α] [inhabited β] :
inhabited (local_equiv α β)
Equations
source
@[protected]
def local_equiv.symm {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
local_equiv β α

The inverse of a local equiv

Equations
source
@[protected, instance]
def local_equiv.has_coe_to_fun {α : Type u_1} {β : Type u_2} :
has_coe_to_fun (local_equiv α β) (λ (_x : local_equiv α β), α → β)
Equations
source
def local_equiv.simps.symm_apply {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
β → α

See Note [custom simps projection]

Equations
source
@[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
source
@[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
source
@[simp]
theorem local_equiv.to_fun_as_coe {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.to_fun = ⇑e
source
@[simp]
theorem local_equiv.inv_fun_as_coe {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.inv_fun = ⇑(e.symm)
source
@[simp]
theorem local_equiv.map_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {x : α} (h : x ∈ e.source) :
⇑e x ∈ e.target
source
@[simp]
theorem local_equiv.map_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {x : β} (h : x ∈ e.target) :
⇑(e.symm) x ∈ e.source
source
@[simp]
theorem local_equiv.left_inv {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {x : α} (h : x ∈ e.source) :
⇑(e.symm) (⇑e x) = x
source
@[simp]
theorem local_equiv.right_inv {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {x : β} (h : x ∈ e.target) :
⇑e (⇑(e.symm) x) = x
source
theorem local_equiv.eq_symm_apply {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.target) :
x = ⇑(e.symm) y ↔ ⇑e x = y
source
@[protected]
theorem local_equiv.maps_to {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
set.maps_to ⇑e e.source e.target
source
theorem local_equiv.symm_maps_to {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
set.maps_to ⇑(e.symm) e.target e.source
source
@[protected]
theorem local_equiv.left_inv_on {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
set.left_inv_on ⇑(e.symm) ⇑e e.source
source
@[protected]
theorem local_equiv.right_inv_on {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
set.right_inv_on ⇑(e.symm) ⇑e e.target
source
@[protected]
theorem local_equiv.inv_on {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
set.inv_on ⇑(e.symm) ⇑e e.source e.target
source
@[protected]
theorem local_equiv.inj_on {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
set.inj_on ⇑e e.source
source
@[protected]
theorem local_equiv.bij_on {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
set.bij_on ⇑e e.source e.target
source
@[protected]
theorem local_equiv.surj_on {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
set.surj_on ⇑e e.source e.target
source
@[simp]
theorem equiv.to_local_equiv_source {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
e.to_local_equiv.source = set.univ
source
@[simp]
theorem equiv.to_local_equiv_target {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
e.to_local_equiv.target = set.univ
source
@[simp]
theorem equiv.to_local_equiv_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
⇑(e.to_local_equiv) = ⇑e
source
@[simp]
theorem equiv.to_local_equiv_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
⇑(e.to_local_equiv.symm) = ⇑(e.symm)
source
def equiv.to_local_equiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
local_equiv α β

Associating a local_equiv to an equiv

Equations
source
@[protected, instance]
def local_equiv.inhabited_of_empty {α : Type u_1} {β : Type u_2} [is_empty α] [is_empty β] :
inhabited (local_equiv α β)
Equations
source
@[simp]
theorem local_equiv.copy_apply {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (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
source
@[simp]
theorem local_equiv.copy_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (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
source
@[simp]
theorem local_equiv.copy_symm_apply {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (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
source
@[simp]
theorem local_equiv.copy_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (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
source
def local_equiv.copy {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑(e.symm) = g) (s : set α) (hs : e.source = s) (t : set β) (ht : e.target = t) :
local_equiv α β

Create a copy of a local_equiv providing better definitional equalities.

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

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

Equations
source
@[simp]
theorem local_equiv.symm_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.symm.source = e.target
source
@[simp]
theorem local_equiv.symm_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.symm.target = e.source
source
@[simp]
theorem local_equiv.symm_symm {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.symm.symm = e
source
theorem local_equiv.image_source_eq_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
⇑e '' e.source = e.target
source
theorem local_equiv.forall_mem_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {p : β → Prop} :
(∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (⇑e x)
source
theorem local_equiv.exists_mem_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {p : β → Prop} :
(∃ (y : β) (H : y ∈ e.target), p y) ↔ ∃ (x : α) (H : x ∈ e.source), p (⇑e x)
source
def local_equiv.is_image {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (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
source
theorem local_equiv.is_image.apply_mem_iff {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} {x : α} (h : e.is_image s t) (hx : x ∈ e.source) :
⇑e x ∈ t ↔ x ∈ s
source
theorem local_equiv.is_image.symm_apply_mem_iff {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : e.is_image s t) ⦃y : β⦄ :
y ∈ e.target → (⇑(e.symm) y ∈ s ↔ y ∈ t)
source
@[protected]
theorem local_equiv.is_image.symm {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : e.is_image s t) :
e.symm.is_image t s
source
@[simp]
theorem local_equiv.is_image.symm_iff {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} :
e.symm.is_image t s ↔ e.is_image s t
source
@[protected]
theorem local_equiv.is_image.maps_to {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : e.is_image s t) :
set.maps_to ⇑e (e.source ∩ s) (e.target ∩ t)
source
theorem local_equiv.is_image.symm_maps_to {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : e.is_image s t) :
set.maps_to ⇑(e.symm) (e.target ∩ t) (e.source ∩ s)
source
@[simp]
theorem local_equiv.is_image.restr_source {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : e.is_image s t) :
h.restr.source = e.source ∩ s
source
@[simp]
theorem local_equiv.is_image.restr_target {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : e.is_image s t) :
h.restr.target = e.target ∩ t
source
@[simp]
theorem local_equiv.is_image.restr_symm_apply {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : e.is_image s t) :
⇑(h.restr.symm) = ⇑(e.symm)
source
def local_equiv.is_image.restr {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : e.is_image s t) :
local_equiv α β

Restrict a local_equiv to a pair of corresponding sets.

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

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

source
theorem local_equiv.is_image.of_preimage_eq {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} :
e.source ∩ ⇑e ⁻¹' t = e.source ∩ s → e.is_image s t

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

source
theorem local_equiv.is_image.iff_symm_preimage_eq {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} :
e.is_image s t ↔ e.target ∩ ⇑(e.symm) ⁻¹' s = e.target ∩ t
source
theorem local_equiv.is_image.symm_preimage_eq {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} :
e.is_image s t → e.target ∩ ⇑(e.symm) ⁻¹' s = e.target ∩ t

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

source
theorem local_equiv.is_image.of_symm_preimage_eq {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} :
e.target ∩ ⇑(e.symm) ⁻¹' s = e.target ∩ t → e.is_image s t

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

source
theorem local_equiv.is_image.of_image_eq {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : ⇑e '' (e.source ∩ s) = e.target ∩ t) :
e.is_image s t
source
theorem local_equiv.is_image.of_symm_image_eq {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : ⇑(e.symm) '' (e.target ∩ t) = e.source ∩ s) :
e.is_image s t
source
@[protected]
theorem local_equiv.is_image.compl {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} (h : e.is_image s t) :
e.is_image sᶜ tᶜ
source
@[protected]
theorem local_equiv.is_image.inter {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {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')
source
@[protected]
theorem local_equiv.is_image.union {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {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')
source
@[protected]
theorem local_equiv.is_image.diff {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {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')
source
theorem local_equiv.is_image.left_inv_on_piecewise {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} {e' : local_equiv α β} [Π (i : α), decidable (i ∈ s)] [Π (i : β), decidable (i ∈ t)] (h : e.is_image s t) (h' : e'.is_image s t) :
set.left_inv_on (t.piecewise ⇑(e.symm) ⇑(e'.symm)) (s.piecewise ⇑e ⇑e') (s.ite e.source e'.source)
source
theorem local_equiv.is_image.inter_eq_of_inter_eq_of_eq_on {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} {e' : local_equiv α β} (h : e.is_image s t) (h' : e'.is_image s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : set.eq_on ⇑e ⇑e' (e.source ∩ s)) :
e.target ∩ t = e'.target ∩ t
source
theorem local_equiv.is_image.symm_eq_on_of_inter_eq_of_eq_on {α : Type u_1} {β : Type u_2} {e : local_equiv α β} {s : set α} {t : set β} {e' : local_equiv α β} (h : e.is_image s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : set.eq_on ⇑e ⇑e' (e.source ∩ s)) :
set.eq_on ⇑(e.symm) ⇑(e'.symm) (e.target ∩ t)
source
theorem local_equiv.is_image_source_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.is_image e.source e.target
source
theorem local_equiv.is_image_source_target_of_disjoint {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (hs : disjoint e.source e'.source) (ht : disjoint e.target e'.target) :
e.is_image e'.source e'.target
source
theorem local_equiv.image_source_inter_eq' {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set α) :
⇑e '' (e.source ∩ s) = e.target ∩ ⇑(e.symm) ⁻¹' s
source
theorem local_equiv.image_source_inter_eq {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set α) :
⇑e '' (e.source ∩ s) = e.target ∩ ⇑(e.symm) ⁻¹' (e.source ∩ s)
source
theorem local_equiv.image_eq_target_inter_inv_preimage {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {s : set α} (h : s ⊆ e.source) :
⇑e '' s = e.target ∩ ⇑(e.symm) ⁻¹' s
source
theorem local_equiv.symm_image_eq_source_inter_preimage {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {s : set β} (h : s ⊆ e.target) :
⇑(e.symm) '' s = e.source ∩ ⇑e ⁻¹' s
source
theorem local_equiv.symm_image_target_inter_eq {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set β) :
⇑(e.symm) '' (e.target ∩ s) = e.source ∩ ⇑e ⁻¹' (e.target ∩ s)
source
theorem local_equiv.symm_image_target_inter_eq' {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set β) :
⇑(e.symm) '' (e.target ∩ s) = e.source ∩ ⇑e ⁻¹' s
source
theorem local_equiv.source_inter_preimage_inv_preimage {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set α) :
e.source ∩ ⇑e ⁻¹' (⇑(e.symm) ⁻¹' s) = e.source ∩ s
source
theorem local_equiv.source_inter_preimage_target_inter {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set β) :
e.source ∩ ⇑e ⁻¹' (e.target ∩ s) = e.source ∩ ⇑e ⁻¹' s
source
theorem local_equiv.target_inter_inv_preimage_preimage {α : Type u_1} {β : Type u_2} (e : local_equiv α β) (s : set β) :
e.target ∩ ⇑(e.symm) ⁻¹' (⇑e ⁻¹' s) = e.target ∩ s
source
theorem local_equiv.symm_image_image_of_subset_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {s : set α} (h : s ⊆ e.source) :
⇑(e.symm) '' (⇑e '' s) = s
source
theorem local_equiv.image_symm_image_of_subset_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) {s : set β} (h : s ⊆ e.target) :
⇑e '' (⇑(e.symm) '' s) = s
source
theorem local_equiv.source_subset_preimage_target {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.source ⊆ ⇑e ⁻¹' e.target
source
theorem local_equiv.symm_image_target_eq_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
⇑(e.symm) '' e.target = e.source
source
theorem local_equiv.target_subset_preimage_source {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.target ⊆ ⇑(e.symm) ⁻¹' e.source
source
@[protected, ext]
theorem local_equiv.ext {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} (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.

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

Restricting a local equivalence to e.source ∩ s

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

The identity local equiv

Equations
source
@[simp]
theorem local_equiv.refl_source {α : Type u_1} :
(local_equiv.refl α).source = set.univ
source
@[simp]
theorem local_equiv.refl_target {α : Type u_1} :
(local_equiv.refl α).target = set.univ
source
@[simp]
theorem local_equiv.refl_coe {α : Type u_1} :
⇑(local_equiv.refl α) = id
source
@[simp]
theorem local_equiv.refl_symm {α : Type u_1} :
(local_equiv.refl α).symm = local_equiv.refl α
source
@[simp]
theorem local_equiv.refl_restr_source {α : Type u_1} (s : set α) :
((local_equiv.refl α).restr s).source = s
source
@[simp]
theorem local_equiv.refl_restr_target {α : Type u_1} (s : set α) :
((local_equiv.refl α).restr s).target = s
source
def local_equiv.of_set {α : Type u_1} (s : set α) :
local_equiv α α

The identity local equiv on a set s

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

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

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

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

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

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

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

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

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

Equations
source
theorem equiv.trans_local_equiv_eq_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : local_equiv β γ) (e : α ≃ β) :
equiv.trans_local_equiv e' e = e.to_local_equiv.trans e'
source
def local_equiv.eq_on_source {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) :
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
source
@[protected, instance]
def local_equiv.eq_on_source_setoid {α : Type u_1} {β : Type u_2} :
setoid (local_equiv α β)

eq_on_source is an equivalence relation

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

Two equivalent local equivs have the same source

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

Two equivalent local equivs coincide on the source

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

Two equivalent local equivs have the same target

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

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

source
theorem local_equiv.eq_on_source.symm_eq_on {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} (h : e ≈ e') :
set.eq_on ⇑(e.symm) ⇑(e'.symm) e.target

Two equivalent local equivs have coinciding inverses on the target

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

Composition of local equivs respects equivalence

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

Restriction of local equivs respects equivalence

source
theorem local_equiv.eq_on_source.source_inter_preimage_eq {α : Type u_1} {β : Type u_2} {e e' : local_equiv α β} (he : e ≈ e') (s : set β) :
e.source ∩ ⇑e ⁻¹' s = e'.source ∩ ⇑e' ⁻¹' s

Preimages are respected by equivalence

source
theorem local_equiv.trans_self_symm {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.trans e.symm ≈ local_equiv.of_set e.source

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

source
theorem local_equiv.trans_symm_self {α : Type u_1} {β : Type u_2} (e : local_equiv α β) :
e.symm.trans e ≈ local_equiv.of_set e.target

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

source
theorem local_equiv.eq_of_eq_on_source_univ {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (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

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

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

Equations
source
@[simp]
theorem local_equiv.prod_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv γ δ) :
(e.prod e').source = e.source ×ˢ e'.source
source
@[simp]
theorem local_equiv.prod_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv γ δ) :
(e.prod e').target = e.target ×ˢ e'.target
source
@[simp]
theorem local_equiv.prod_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv γ δ) :
⇑(e.prod e') = λ (p : α × γ), (⇑e p.fst, ⇑e' p.snd)
source
theorem local_equiv.prod_coe_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv γ δ) :
⇑((e.prod e').symm) = λ (p : β × δ), (⇑(e.symm) p.fst, ⇑(e'.symm) p.snd)
source
@[simp]
theorem local_equiv.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : local_equiv α β) (e' : local_equiv γ δ) :
(e.prod e').symm = e.symm.prod e'.symm
source
@[simp]
theorem local_equiv.refl_prod_refl {α : Type u_1} {β : Type u_2} :
(local_equiv.refl α).prod (local_equiv.refl β) = local_equiv.refl (α × β)
source
@[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 : local_equiv α β) (f : local_equiv β γ) (e' : local_equiv δ η) (f' : local_equiv η ε) :
(e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
source
def local_equiv.piecewise {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (s : set α) (t : set β) [Π (x : α), decidable (x ∈ s)] [Π (y : β), decidable (y ∈ t)] (H : e.is_image s t) (H' : e'.is_image s t) :
local_equiv α β

Combine two local_equivs 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
source
@[simp]
theorem local_equiv.piecewise_source {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (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
source
@[simp]
theorem local_equiv.piecewise_symm_apply {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (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)
source
@[simp]
theorem local_equiv.piecewise_apply {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (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'
source
@[simp]
theorem local_equiv.piecewise_target {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (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
source
theorem local_equiv.symm_piecewise {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) {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 _ _
source
@[simp]
theorem local_equiv.disjoint_union_source {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (hs : disjoint e.source e'.source) (ht : disjoint e.target e'.target) [Π (x : α), decidable (x ∈ e.source)] [Π (y : β), decidable (y ∈ e.target)] :
(e.disjoint_union e' hs ht).source = e.source ∪ e'.source
source
def local_equiv.disjoint_union {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (hs : disjoint e.source e'.source) (ht : disjoint e.target e'.target) [Π (x : α), decidable (x ∈ e.source)] [Π (y : β), decidable (y ∈ e.target)] :
local_equiv α β

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

Equations
source
@[simp]
theorem local_equiv.disjoint_union_symm_apply {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (hs : disjoint e.source e'.source) (ht : disjoint e.target e'.target) [Π (x : α), decidable (x ∈ e.source)] [Π (y : β), decidable (y ∈ e.target)] :
⇑((e.disjoint_union e' hs ht).symm) = e.target.piecewise ⇑(e.symm) ⇑(e'.symm)
source
@[simp]
theorem local_equiv.disjoint_union_target {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (hs : disjoint e.source e'.source) (ht : disjoint e.target e'.target) [Π (x : α), decidable (x ∈ e.source)] [Π (y : β), decidable (y ∈ e.target)] :
(e.disjoint_union e' hs ht).target = e.target ∪ e'.target
source
@[simp]
theorem local_equiv.disjoint_union_apply {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (hs : disjoint e.source e'.source) (ht : disjoint e.target e'.target) [Π (x : α), decidable (x ∈ e.source)] [Π (y : β), decidable (y ∈ e.target)] :
⇑(e.disjoint_union e' hs ht) = e.source.piecewise ⇑e ⇑e'
source
theorem local_equiv.disjoint_union_eq_piecewise {α : Type u_1} {β : Type u_2} (e e' : local_equiv α β) (hs : disjoint e.source e'.source) (ht : disjoint e.target 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 _ _
source
@[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
source
@[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)
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)
source
@[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)
source
@[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)
source
@[simp]
theorem set.bij_on.to_local_equiv_source {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) (t : set β) (hf : set.bij_on f s t) :
(set.bij_on.to_local_equiv f s t hf).source = s
source
@[simp]
theorem set.bij_on.to_local_equiv_symm_apply {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) (t : set β) (hf : set.bij_on f s t) :
⇑((set.bij_on.to_local_equiv f s t hf).symm) = function.inv_fun_on f s
source
@[simp]
theorem set.bij_on.to_local_equiv_target {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) (t : set β) (hf : set.bij_on f s t) :
(set.bij_on.to_local_equiv f s t hf).target = t
source
@[simp]
theorem set.bij_on.to_local_equiv_apply {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) (t : set β) (hf : set.bij_on f s t) :
⇑(set.bij_on.to_local_equiv f s t hf) = f
source
noncomputable def set.bij_on.to_local_equiv {α : Type u_1} {β : Type u_2} [nonempty α] (f : α → β) (s : set α) (t : set β) (hf : set.bij_on f s t) :
local_equiv α β

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

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

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

Equations
source
@[simp]
theorem equiv.refl_to_local_equiv {α : Type u_1} :
(equiv.refl α).to_local_equiv = local_equiv.refl α
source
@[simp]
theorem equiv.symm_to_local_equiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
e.symm.to_local_equiv = e.to_local_equiv.symm
source
@[simp]
theorem equiv.trans_to_local_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (e' : β ≃ γ) :
(e.trans e').to_local_equiv = e.to_local_equiv.trans e'.to_local_equiv