mathlib3 documentation

topology.local_homeomorph

Local homeomorphisms #

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

This file defines homeomorphisms between open subsets of topological spaces. An element e of local_homeomorph α β is an extension of local_equiv α β, i.e., it is a pair of functions e.to_fun and e.inv_fun, inverse of each other on the sets e.source and e.target. Additionally, we require that these sets are open, and that the functions are continuous on them. Equivalently, they are homeomorphisms there.

As in equivs, we register a coercion to functions, and we use e x and e.symm x throughout instead of e.to_fun x and e.inv_fun x.

Main definitions #

homeomorph.to_local_homeomorph: associating a local homeomorphism to a homeomorphism, with source = target = univ local_homeomorph.symm : the inverse of a local homeomorphism local_homeomorph.trans : the composition of two local homeomorphisms local_homeomorph.refl : the identity local homeomorphism local_homeomorph.of_set: the identity on a set s eq_on_source : equivalence relation describing the "right" notion of equality for local homeomorphisms

Implementation notes #

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

For design notes, see local_equiv.lean.

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.

@[nolint]
structure local_homeomorph (α : Type u_5) (β : Type u_6) [topological_space α] [topological_space β] :
Type (max u_5 u_6)

local homeomorphisms, defined on open subsets of the space

Instances for local_homeomorph
@[protected, instance]
def local_homeomorph.has_coe_to_fun {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
has_coe_to_fun (local_homeomorph α β) (λ (_x : local_homeomorph α β), α β)
Equations
@[protected]
def local_homeomorph.symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :

The inverse of a local homeomorphism

Equations
def local_homeomorph.simps.apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :
α β

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
@[simp]
theorem local_homeomorph.coe_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :
@[simp]
@[simp]
theorem local_homeomorph.map_source {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (h : x e.to_local_equiv.source) :
@[simp]
theorem local_homeomorph.map_target {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : β} (h : x e.to_local_equiv.target) :
@[simp]
theorem local_homeomorph.left_inv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (h : x e.to_local_equiv.source) :
(e.symm) (e x) = x
@[simp]
theorem local_homeomorph.right_inv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : β} (h : x e.to_local_equiv.target) :
e ((e.symm) x) = x
theorem local_homeomorph.eq_symm_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} {y : β} (hx : x e.to_local_equiv.source) (hy : y e.to_local_equiv.target) :
x = (e.symm) y e x = y
@[protected]
@[simp]
def local_homeomorph.replace_equiv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) (e' : local_equiv α β) (h : e.to_local_equiv = e') :

Replace to_local_equiv field to provide better definitional equalities.

Equations
theorem local_homeomorph.replace_equiv_eq_self {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) (e' : local_equiv α β) (h : e.to_local_equiv = e') :
e.replace_equiv e' h = e
theorem local_homeomorph.eventually_left_inverse {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (hx : x e.to_local_equiv.source) :
∀ᶠ (y : α) in nhds x, (e.symm) (e y) = y
theorem local_homeomorph.eventually_left_inverse' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : β} (hx : x e.to_local_equiv.target) :
∀ᶠ (y : α) in nhds ((e.symm) x), (e.symm) (e y) = y
theorem local_homeomorph.eventually_right_inverse {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : β} (hx : x e.to_local_equiv.target) :
∀ᶠ (y : β) in nhds x, e ((e.symm) y) = y
theorem local_homeomorph.eventually_right_inverse' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (hx : x e.to_local_equiv.source) :
∀ᶠ (y : β) in nhds (e x), e ((e.symm) y) = y
theorem local_homeomorph.eventually_ne_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (hx : x e.to_local_equiv.source) :
∀ᶠ (x' : α) in nhds_within x {x}, e x' e x
@[protected, ext]
theorem local_homeomorph.ext {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e e' : local_homeomorph α β) (h : (x : α), e x = e' x) (hinv : (x : β), (e.symm) x = (e'.symm) x) (hs : e.to_local_equiv.source = e'.to_local_equiv.source) :
e = e'

Two local homeomorphisms are equal when they have equal to_fun, inv_fun and source. It is not sufficient to have equal to_fun and source, as this only determines inv_fun on the target. This would only be true for a weaker notion of equality, arguably the right one, called eq_on_source.

@[protected]
theorem local_homeomorph.ext_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e e' : local_homeomorph α β} :
e = e' ( (x : α), e x = e' x) ( (x : β), (e.symm) x = (e'.symm) x) e.to_local_equiv.source = e'.to_local_equiv.source
@[simp]
theorem local_homeomorph.symm_symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :
e.symm.symm = e
@[protected]
theorem local_homeomorph.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (h : x e.to_local_equiv.source) :

A local homeomorphism is continuous at any point of its source

theorem local_homeomorph.continuous_at_symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : β} (h : x e.to_local_equiv.target) :

A local homeomorphism inverse is continuous at any point of its target

theorem local_homeomorph.tendsto_symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (hx : x e.to_local_equiv.source) :
theorem local_homeomorph.map_nhds_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (hx : x e.to_local_equiv.source) :
theorem local_homeomorph.symm_map_nhds_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (hx : x e.to_local_equiv.source) :
theorem local_homeomorph.image_mem_nhds {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (hx : x e.to_local_equiv.source) {s : set α} (hs : s nhds x) :
e '' s nhds (e x)
theorem local_homeomorph.map_nhds_within_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (hx : x e.to_local_equiv.source) (s : set α) :
theorem local_homeomorph.eventually_nhds {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (p : β Prop) (hx : x e.to_local_equiv.source) :
(∀ᶠ (y : β) in nhds (e x), p y) ∀ᶠ (x : α) in nhds x, p (e x)
theorem local_homeomorph.eventually_nhds' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (p : α Prop) (hx : x e.to_local_equiv.source) :
(∀ᶠ (y : β) in nhds (e x), p ((e.symm) y)) ∀ᶠ (x : α) in nhds x, p x
theorem local_homeomorph.eventually_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (p : β Prop) {s : set α} (hx : x e.to_local_equiv.source) :
(∀ᶠ (y : β) in nhds_within (e x) ((e.symm) ⁻¹' s), p y) ∀ᶠ (x : α) in nhds_within x s, p (e x)
theorem local_homeomorph.eventually_nhds_within' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} (p : α Prop) {s : set α} (hx : x e.to_local_equiv.source) :
(∀ᶠ (y : β) in nhds_within (e x) ((e.symm) ⁻¹' s), p ((e.symm) y)) ∀ᶠ (x : α) in nhds_within x s, p x
theorem local_homeomorph.preimage_eventually_eq_target_inter_preimage_inter {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {e : local_homeomorph α β} {s : set α} {t : set γ} {x : α} {f : α γ} (hf : continuous_within_at f s x) (hxe : x e.to_local_equiv.source) (ht : t nhds (f x)) :

This lemma is useful in the manifold library in the case that e is a chart. It states that locally around e x the set e.symm ⁻¹' s is the same as the set intersected with the target of e and some other neighborhood of f x (which will be the source of a chart on γ).

local_homeomorph.is_image relation #

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

This definition is a restatement of local_equiv.is_image for local homeomorphisms. In this section we transfer API about local_equiv.is_image to local homeomorphisms and add a few local_homeomorph-specific lemmas like local_homeomorph.is_image.closure.

def local_homeomorph.is_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) (s : set α) (t : set β) :
Prop

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

  • e '' (e.source ∩ s) = e.target ∩ t;
  • e.source ∩ e ⁻¹ t = e.source ∩ s;
  • ∀ x ∈ e.source, e x ∈ t ↔ x ∈ s (this one is used in the definition).
Equations
theorem local_homeomorph.is_image.to_local_equiv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_homeomorph.is_image.apply_mem_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} {x : α} (h : e.is_image s t) (hx : x e.to_local_equiv.source) :
e x t x s
@[protected]
theorem local_homeomorph.is_image.symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_homeomorph.is_image.symm_apply_mem_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} {y : β} (h : e.is_image s t) (hy : y e.to_local_equiv.target) :
(e.symm) y s y t
@[simp]
theorem local_homeomorph.is_image.symm_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} :
@[protected]
theorem local_homeomorph.is_image.maps_to {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_homeomorph.is_image.symm_maps_to {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_homeomorph.is_image.image_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_homeomorph.is_image.symm_image_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) :

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

Alias of the reverse direction of local_homeomorph.is_image.iff_symm_preimage_eq'.

Alias of the forward direction of local_homeomorph.is_image.iff_symm_preimage_eq'.

Alias of the forward direction of local_homeomorph.is_image.iff_preimage_eq'.

Alias of the reverse direction of local_homeomorph.is_image.iff_preimage_eq'.

theorem local_homeomorph.is_image.of_image_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e '' (e.to_local_equiv.source s) = e.to_local_equiv.target t) :
e.is_image s t
theorem local_homeomorph.is_image.of_symm_image_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : (e.symm) '' (e.to_local_equiv.target t) = e.to_local_equiv.source s) :
e.is_image s t
@[protected]
theorem local_homeomorph.is_image.compl {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) :
@[protected]
theorem local_homeomorph.is_image.inter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {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_homeomorph.is_image.union {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {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_homeomorph.is_image.diff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {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_homeomorph.is_image.left_inv_on_piecewise {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} {e' : local_homeomorph α β} [Π (i : α), decidable (i s)] [Π (i : β), decidable (i t)] (h : e.is_image s t) (h' : e'.is_image s t) :
theorem local_homeomorph.is_image.map_nhds_within_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} {x : α} (h : e.is_image s t) (hx : x e.to_local_equiv.source) :
@[protected]
theorem local_homeomorph.is_image.closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) :
@[protected]
theorem local_homeomorph.is_image.interior {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) :
@[protected]
theorem local_homeomorph.is_image.frontier {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) :
def local_homeomorph.is_image.restr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) (hs : is_open (e.to_local_equiv.source s)) :

Restrict a local_homeomorph to a pair of corresponding open sets.

Equations
@[simp]
theorem local_homeomorph.is_image.restr_to_local_equiv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} {t : set β} (h : e.is_image s t) (hs : is_open (e.to_local_equiv.source s)) :

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

theorem local_homeomorph.image_open_of_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {s : set α} (hs : is_open s) (h : s e.to_local_equiv.source) :

The image of an open set in the source is open.

theorem local_homeomorph.image_open_of_open' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {s : set α} (hs : is_open s) :

The image of the restriction of an open set to the source is open.

A local_equiv with continuous open forward map and an open source is a local_homeomorph.

Equations

A local_equiv with continuous open forward map and an open source is a local_homeomorph.

Equations
@[protected]
def local_homeomorph.restr_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) (s : set α) (hs : is_open s) :

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

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

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

Equations
@[simp]
theorem local_homeomorph.restr_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) (s : set α) :
(e.restr s) = e
@[simp]
theorem local_homeomorph.restr_symm_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) (s : set α) :
((e.restr s).symm) = (e.symm)
theorem local_homeomorph.restr_eq_of_source_subset {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} (h : e.to_local_equiv.source s) :
e.restr s = e
@[simp]
theorem local_homeomorph.restr_univ {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} :
theorem local_homeomorph.restr_source_inter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) (s : set α) :
@[protected]

The identity on the whole space as a local homeomorphism.

Equations
@[protected]

Composition of two local homeomorphisms when the target of the first and the source of the second coincide.

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

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

Equations
@[simp]
theorem local_homeomorph.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : local_homeomorph β γ) :
(e.trans e') = e' e
@[simp]
theorem local_homeomorph.coe_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : local_homeomorph β γ) :
((e.trans e').symm) = (e.symm) (e'.symm)
theorem local_homeomorph.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : local_homeomorph β γ) {x : α} :
(e.trans e') x = e' (e x)
theorem local_homeomorph.trans_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] (e : local_homeomorph α β) (e' : local_homeomorph β γ) (e'' : local_homeomorph γ δ) :
(e.trans e').trans e'' = e.trans (e'.trans e'')
@[simp]
@[simp]
theorem local_homeomorph.trans_of_set {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {s : set β} (hs : is_open s) :
theorem local_homeomorph.of_set_trans {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {s : set α} (hs : is_open s) :
@[simp]
theorem local_homeomorph.of_set_trans_of_set {α : Type u_1} [topological_space α] {s : set α} (hs : is_open s) {s' : set α} (hs' : is_open s') :
theorem local_homeomorph.restr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : local_homeomorph β γ) (s : set α) :
(e.restr s).trans e' = (e.trans e').restr s
def local_homeomorph.trans_homeomorph {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : β ≃ₜ γ) :

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

Equations
@[simp]
theorem local_homeomorph.trans_homeomorph_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : β ≃ₜ γ) :
@[simp]
theorem local_homeomorph.trans_homeomorph_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : β ≃ₜ γ) :
def homeomorph.trans_local_homeomorph {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e' : local_homeomorph β γ) (e : α ≃ₜ β) :

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

Equations
@[simp]
def local_homeomorph.eq_on_source {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e e' : local_homeomorph α β) :
Prop

eq_on_source e e' means that e and e' have the same source, and coincide there. They should really be considered the same local equiv.

Equations
@[protected, instance]

eq_on_source is an equivalence relation

Equations
theorem local_homeomorph.eq_on_source_refl {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :
e e
theorem local_homeomorph.eq_on_source.symm' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e e' : local_homeomorph α β} (h : e e') :

If two local homeomorphisms are equivalent, so are their inverses

Two equivalent local homeomorphisms have the same source

Two equivalent local homeomorphisms have the same target

Two equivalent local homeomorphisms have coinciding to_fun on the source

Two equivalent local homeomorphisms have coinciding inv_fun on the target

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

Composition of local homeomorphisms respects equivalence

theorem local_homeomorph.eq_on_source.restr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e e' : local_homeomorph α β} (he : e e') (s : set α) :
e.restr s e'.restr s

Restriction of local homeomorphisms respects equivalence

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

@[simp]
theorem local_homeomorph.prod_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] (e : local_homeomorph α β) (e' : local_homeomorph γ δ) :
(e.prod e') = λ (p : α × γ), (e p.fst, e' p.snd)
def local_homeomorph.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] (e : local_homeomorph α β) (e' : local_homeomorph γ δ) :
local_homeomorph × γ) × δ)

The product of two local homeomorphisms, as a local homeomorphism on the product space.

Equations
theorem local_homeomorph.prod_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] (e : local_homeomorph α β) (e' : local_homeomorph γ δ) (p : β × δ) :
((e.prod e').symm) p = ((e.symm) p.fst, (e'.symm) p.snd)
@[simp]
theorem local_homeomorph.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] (e : local_homeomorph α β) (e' : local_homeomorph γ δ) :
(e.prod e').symm = e.symm.prod e'.symm
@[simp]
theorem local_homeomorph.prod_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {η : Type u_5} {ε : Type u_6} [topological_space η] [topological_space ε] (e : local_homeomorph α β) (f : local_homeomorph β γ) (e' : local_homeomorph δ η) (f' : local_homeomorph η ε) :
(e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
theorem local_homeomorph.prod_eq_prod_of_nonempty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {e₁ e₁' : local_homeomorph α β} {e₂ e₂' : local_homeomorph γ δ} (h : (e₁.prod e₂).to_local_equiv.source.nonempty) :
e₁.prod e₂ = e₁'.prod e₂' e₁ = e₁' e₂ = e₂'
theorem local_homeomorph.prod_eq_prod_of_nonempty' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {e₁ e₁' : local_homeomorph α β} {e₂ e₂' : local_homeomorph γ δ} (h : (e₁'.prod e₂').to_local_equiv.source.nonempty) :
e₁.prod e₂ = e₁'.prod e₂' e₁ = e₁' e₂ = e₂'
@[simp]
theorem local_homeomorph.piecewise_to_local_equiv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e e' : local_homeomorph α β) (s : set α) (t : set β) [Π (x : α), decidable (x s)] [Π (y : β), decidable (y t)] (H : e.is_image s t) (H' : e'.is_image s t) (Hs : e.to_local_equiv.source frontier s = e'.to_local_equiv.source frontier s) (Heq : set.eq_on e e' (e.to_local_equiv.source frontier s)) :
(e.piecewise e' s t H H' Hs Heq).to_local_equiv = e.to_local_equiv.piecewise e'.to_local_equiv s t H H'
def local_homeomorph.piecewise {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e e' : local_homeomorph α β) (s : set α) (t : set β) [Π (x : α), decidable (x s)] [Π (y : β), decidable (y t)] (H : e.is_image s t) (H' : e'.is_image s t) (Hs : e.to_local_equiv.source frontier s = e'.to_local_equiv.source frontier s) (Heq : set.eq_on e e' (e.to_local_equiv.source frontier s)) :

Combine two local_homeomorphs using set.piecewise. The source of the new local_homeomorph 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. To ensure that the maps to_fun and inv_fun are inverse of each other on the new source and target, the definition assumes that the sets s and t are related both by e.is_image and e'.is_image. To ensure that the new maps are continuous on source/target, it also assumes that e.source and e'.source meet frontier s on the same set and e x = e' x on this intersection.

Equations
@[simp]
theorem local_homeomorph.piecewise_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e e' : local_homeomorph α β) (s : set α) (t : set β) [Π (x : α), decidable (x s)] [Π (y : β), decidable (y t)] (H : e.is_image s t) (H' : e'.is_image s t) (Hs : e.to_local_equiv.source frontier s = e'.to_local_equiv.source frontier s) (Heq : set.eq_on e e' (e.to_local_equiv.source frontier s)) :
(e.piecewise e' s t H H' Hs Heq) = s.piecewise e e'
@[simp]
theorem local_homeomorph.symm_piecewise {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e e' : local_homeomorph α β) {s : set α} {t : set β} [Π (x : α), decidable (x s)] [Π (y : β), decidable (y t)] (H : e.is_image s t) (H' : e'.is_image s t) (Hs : e.to_local_equiv.source frontier s = e'.to_local_equiv.source frontier s) (Heq : set.eq_on e e' (e.to_local_equiv.source frontier s)) :
(e.piecewise e' s t H H' Hs Heq).symm = e.symm.piecewise e'.symm t s _ _ _ _

Combine two local_homeomorphs with disjoint sources and disjoint targets. We reuse local_homeomorph.piecewise then override to_local_equiv to local_equiv.disjoint_union. This way we have better definitional equalities for source and target.

Equations
def local_homeomorph.pi {ι : Type u_5} [fintype ι] {Xi : ι Type u_6} {Yi : ι Type u_7} [Π (i : ι), topological_space (Xi i)] [Π (i : ι), topological_space (Yi i)] (ei : Π (i : ι), local_homeomorph (Xi i) (Yi i)) :
local_homeomorph (Π (i : ι), Xi i) (Π (i : ι), Yi i)

The product of a finite family of local_homeomorphs.

Equations
@[simp]
theorem local_homeomorph.pi_to_local_equiv {ι : Type u_5} [fintype ι] {Xi : ι Type u_6} {Yi : ι Type u_7} [Π (i : ι), topological_space (Xi i)] [Π (i : ι), topological_space (Yi i)] (ei : Π (i : ι), local_homeomorph (Xi i) (Yi i)) :

Continuity within a set at a point can be read under right composition with a local homeomorphism, if the point is in its target

theorem local_homeomorph.continuous_at_iff_continuous_at_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) {f : β γ} {x : β} (h : x e.to_local_equiv.target) :

Continuity at a point can be read under right composition with a local homeomorphism, if the point is in its target

A function is continuous on a set if and only if its composition with a local homeomorphism on the right is continuous on the corresponding set.

Continuity within a set at a point can be read under left composition with a local homeomorphism if a neighborhood of the initial point is sent to the source of the local homeomorphism

Continuity at a point can be read under left composition with a local homeomorphism if a neighborhood of the initial point is sent to the source of the local homeomorphism

A function is continuous on a set if and only if its composition with a local homeomorphism on the left is continuous on the corresponding set.

A function is continuous if and only if its composition with a local homeomorphism on the left is continuous and its image is contained in the source.

def local_homeomorph.homeomorph_of_image_subset_source {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {s : set α} {t : set β} (hs : s e.to_local_equiv.source) (ht : e '' s = t) :

The homeomorphism obtained by restricting a local_homeomorph to a subset of the source.

Equations
@[simp]
theorem local_homeomorph.homeomorph_of_image_subset_source_apply_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {s : set α} {t : set β} (hs : s e.to_local_equiv.source) (ht : e '' s = t) (a : s) :
@[simp]
theorem local_homeomorph.homeomorph_of_image_subset_source_symm_apply_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {s : set α} {t : set β} (hs : s e.to_local_equiv.source) (ht : e '' s = t) (b : t) :

A local homeomrphism defines a homeomorphism between its source and target.

Equations

If a local homeomorphism has source and target equal to univ, then it induces a homeomorphism between the whole spaces, expressed in this definition.

Equations

A local homeomorphism whose source is all of α defines an open embedding of α into β. The converse is also true; see open_embedding.to_local_homeomorph.

noncomputable def open_embedding.to_local_homeomorph {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α β) (h : open_embedding f) [nonempty α] :

An open embedding of α into β, with α nonempty, defines a local homeomorphism whose source is all of α. The converse is also true; see local_homeomorph.to_open_embedding.

Equations
theorem open_embedding.continuous_at_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α β} {g : β γ} (hf : open_embedding f) {x : α} :

The inclusion of an open subset s of a space α into α is a local homeomorphism from the subtype s to α.

Equations

The restriction of a local homeomorphism e to an open subset s of the domain type produces a local homeomorphism whose domain is the subtype s.

Equations