mathlibdocumentation

topology.local_homeomorph

Local homeomorphisms #

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)  :
Type (max u_5 u_6)
• to_local_equiv : β
• open_source :
• open_target :
• continuous_to_fun :
• continuous_inv_fun :

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}  :
(λ (_x : β), α → β)
Equations
@[protected]
def local_homeomorph.symm {α : Type u_1} {β : Type u_2} (e : β) :

The inverse of a local homeomorphism

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

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

Equations
def local_homeomorph.simps.symm_apply {α : Type u_1} {β : Type u_2} (e : β) :
β → α
Equations
@[protected]
theorem local_homeomorph.continuous_on {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_homeomorph.continuous_on_symm {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem local_homeomorph.mk_coe {α : Type u_1} {β : Type u_2} (e : β) (a : is_open e.source) (b : is_open e.target) (c : e.source) (d : e.target) :
@[simp]
theorem local_homeomorph.mk_coe_symm {α : Type u_1} {β : Type u_2} (e : β) (a : is_open e.source) (b : is_open e.target) (c : e.source) (d : e.target) :
theorem local_homeomorph.to_local_equiv_injective {α : Type u_1} {β : Type u_2}  :
@[simp]
theorem local_homeomorph.to_fun_eq_coe {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem local_homeomorph.inv_fun_eq_coe {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem local_homeomorph.coe_coe {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem local_homeomorph.coe_coe_symm {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem local_homeomorph.map_source {α : Type u_1} {β : Type u_2} (e : β) {x : α} (h : x e.to_local_equiv.source) :
@[simp]
theorem local_homeomorph.map_target {α : Type u_1} {β : Type u_2} (e : β) {x : β} (h : x e.to_local_equiv.target) :
@[simp]
theorem local_homeomorph.left_inv {α : Type u_1} {β : Type u_2} (e : β) {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} (e : β) {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} (e : β) {x : α} {y : β} (hx : x e.to_local_equiv.source) (hy : y e.to_local_equiv.target) :
x = (e.symm) y e x = y
@[protected]
theorem local_homeomorph.maps_to {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_homeomorph.symm_maps_to {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_homeomorph.left_inv_on {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_homeomorph.right_inv_on {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_homeomorph.inv_on {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_homeomorph.inj_on {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_homeomorph.bij_on {α : Type u_1} {β : Type u_2} (e : β) :
@[protected]
theorem local_homeomorph.surj_on {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem homeomorph.to_local_homeomorph_target {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) :
@[simp]
theorem homeomorph.to_local_homeomorph_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) :
def homeomorph.to_local_homeomorph {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) :

A homeomorphism induces a local homeomorphism on the whole space

Equations
@[simp]
theorem homeomorph.to_local_homeomorph_source {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) :
@[simp]
theorem homeomorph.to_local_homeomorph_apply {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) :
def local_homeomorph.replace_equiv {α : Type u_1} {β : Type u_2} (e : β) (e' : β) (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} (e : β) (e' : β) (h : e.to_local_equiv = e') :
e.replace_equiv e' h = e
theorem local_homeomorph.source_preimage_target {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_homeomorph.eq_of_local_equiv_eq {α : Type u_1} {β : Type u_2} {e e' : β} (h : e.to_local_equiv = e'.to_local_equiv) :
e = e'
theorem local_homeomorph.eventually_left_inverse {α : Type u_1} {β : Type u_2} (e : β) {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} (e : β) {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} (e : β) {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} (e : β) {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} (e : β) {x : α} (hx : x e.to_local_equiv.source) :
∀ᶠ (x' : α) in {x}, e x' e x
theorem local_homeomorph.nhds_within_source_inter {α : Type u_1} {β : Type u_2} (e : β) {x : α} (hx : x e.to_local_equiv.source) (s : set α) :
theorem local_homeomorph.nhds_within_target_inter {α : Type u_1} {β : Type u_2} (e : β) {x : β} (hx : x e.to_local_equiv.target) (s : set β) :
theorem local_homeomorph.image_eq_target_inter_inv_preimage {α : Type u_1} {β : Type u_2} (e : β) {s : set α} (h : s e.to_local_equiv.source) :
theorem local_homeomorph.image_source_inter_eq' {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
theorem local_homeomorph.image_source_inter_eq {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
theorem local_homeomorph.symm_image_eq_source_inter_preimage {α : Type u_1} {β : Type u_2} (e : β) {s : set β} (h : s e.to_local_equiv.target) :
theorem local_homeomorph.symm_image_target_inter_eq {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :
theorem local_homeomorph.source_inter_preimage_inv_preimage {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
theorem local_homeomorph.target_inter_inv_preimage_preimage {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :
theorem local_homeomorph.image_source_eq_target {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_homeomorph.symm_image_target_eq_source {α : Type u_1} {β : Type u_2} (e : β) :
@[protected, ext]
theorem local_homeomorph.ext {α : Type u_1} {β : Type u_2} (e e' : β) (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} {e e' : β} :
e = e' (∀ (x : α), e x = e' x) (∀ (x : β), (e.symm) x = (e'.symm) x)
@[simp]
theorem local_homeomorph.symm_to_local_equiv {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_homeomorph.symm_source {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_homeomorph.symm_target {α : Type u_1} {β : Type u_2} (e : β) :
@[simp]
theorem local_homeomorph.symm_symm {α : Type u_1} {β : Type u_2} (e : β) :
e.symm.symm = e
@[protected]
theorem local_homeomorph.continuous_at {α : Type u_1} {β : Type u_2} (e : β) {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} (e : β) {x : β} (h : x e.to_local_equiv.target) :
x

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

theorem local_homeomorph.tendsto_symm {α : Type u_1} {β : Type u_2} (e : β) {x : α} (hx : x e.to_local_equiv.source) :
(nhds (e x)) (nhds x)
theorem local_homeomorph.map_nhds_eq {α : Type u_1} {β : Type u_2} (e : β) {x : α} (hx : x e.to_local_equiv.source) :
(nhds x) = nhds (e x)
theorem local_homeomorph.symm_map_nhds_eq {α : Type u_1} {β : Type u_2} (e : β) {x : α} (hx : x e.to_local_equiv.source) :
theorem local_homeomorph.image_mem_nhds {α : Type u_1} {β : Type u_2} (e : β) {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} (e : β) {x : α} (hx : x e.to_local_equiv.source) (s : set α) :
theorem local_homeomorph.map_nhds_within_preimage_eq {α : Type u_1} {β : Type u_2} (e : β) {x : α} (hx : x e.to_local_equiv.source) (s : set β) :
(e ⁻¹' s)) = nhds_within (e x) s
theorem local_homeomorph.eventually_nhds {α : Type u_1} {β : Type u_2} (e : β) {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} (e : β) {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} (e : β) {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 s, p (e x)
theorem local_homeomorph.eventually_nhds_within' {α : Type u_1} {β : Type u_2} (e : β) {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 s, p x
theorem local_homeomorph.preimage_eventually_eq_target_inter_preimage_inter {α : Type u_1} {β : Type u_2} {γ : Type u_3} {e : β} {s : set α} {t : set γ} {x : α} {f : α → γ} (hf : 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 `γ`).

theorem local_homeomorph.preimage_open_of_open {α : Type u_1} {β : Type u_2} (e : β) {s : set β} (hs : is_open s) :

`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:

• `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).

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} (e : β) (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} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
t
theorem local_homeomorph.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.to_local_equiv.source) :
e x t x s
@[protected]
theorem local_homeomorph.is_image.symm {α : Type u_1} {β : Type u_2} {e : β} {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} {e : β} {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} {e : β} {s : set α} {t : set β} :
@[protected]
theorem local_homeomorph.is_image.maps_to {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_homeomorph.is_image.symm_maps_to {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_homeomorph.is_image.image_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_homeomorph.is_image.symm_image_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_homeomorph.is_image.iff_preimage_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :
theorem local_homeomorph.is_image.preimage_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :

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

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

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

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

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

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

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

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

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

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

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

theorem local_homeomorph.is_image.iff_preimage_eq' {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :
theorem local_homeomorph.is_image.preimage_eq' {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} :

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

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

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} {e : β} {s : set α} {t : set β} (h : e '' (e.to_local_equiv.source s) = ) :
e.is_image s t
theorem local_homeomorph.is_image.of_symm_image_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : (e.symm) '' (e.to_local_equiv.target t) = ) :
e.is_image s t
@[protected]
theorem local_homeomorph.is_image.compl {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
@[protected]
theorem local_homeomorph.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_homeomorph.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_homeomorph.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_homeomorph.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_homeomorph.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 : = ) (Heq : e' (e.to_local_equiv.source s)) :
=
theorem local_homeomorph.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 : = ) (Heq : e' (e.to_local_equiv.source s)) :
theorem local_homeomorph.is_image.map_nhds_within_eq {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} {x : α} (h : e.is_image s t) (hx : x e.to_local_equiv.source) :
s) = nhds_within (e x) t
@[protected]
theorem local_homeomorph.is_image.closure {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
@[protected]
theorem local_homeomorph.is_image.interior {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
@[protected]
theorem local_homeomorph.is_image.frontier {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
theorem local_homeomorph.is_image.is_open_iff {α : Type u_1} {β : Type u_2} {e : β} {s : set α} {t : set β} (h : e.is_image s t) :
def local_homeomorph.is_image.restr {α : Type u_1} {β : Type u_2} {e : β} {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} {e : β} {s : set α} {t : set β} (h : e.is_image s t) (hs : is_open (e.to_local_equiv.source s)) :
theorem local_homeomorph.is_image_source_target {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_homeomorph.is_image_source_target_of_disjoint {α : Type u_1} {β : Type u_2} (e e' : β) (hs : e'.to_local_equiv.source) (ht : e'.to_local_equiv.target) :
theorem local_homeomorph.preimage_interior {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :

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

theorem local_homeomorph.preimage_closure {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :
theorem local_homeomorph.preimage_frontier {α : Type u_1} {β : Type u_2} (e : β) (s : set β) :
theorem local_homeomorph.preimage_open_of_open_symm {α : Type u_1} {β : Type u_2} (e : β) {s : set α} (hs : is_open s) :
theorem local_homeomorph.image_open_of_open {α : Type u_1} {β : Type u_2} (e : β) {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} (e : β) {s : set α} (hs : is_open s) :

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

def local_homeomorph.of_continuous_open_restrict {α : Type u_1} {β : Type u_2} (e : β) (hc : e.source) (ho : is_open_map (e.source.restrict e)) (hs : is_open e.source) :

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

Equations
def local_homeomorph.of_continuous_open {α : Type u_1} {β : Type u_2} (e : β) (hc : e.source) (ho : is_open_map e) (hs : is_open e.source) :

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

Equations
• hs =
@[protected]
def local_homeomorph.restr_open {α : Type u_1} {β : Type u_2} (e : β) (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]
theorem local_homeomorph.restr_open_to_local_equiv {α : Type u_1} {β : Type u_2} (e : β) (s : set α) (hs : is_open s) :
theorem local_homeomorph.restr_open_source {α : Type u_1} {β : Type u_2} (e : β) (s : set α) (hs : is_open s) :
theorem local_homeomorph.restr_target {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
@[protected]
def local_homeomorph.restr {α : Type u_1} {β : Type u_2} (e : β) (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
theorem local_homeomorph.restr_source {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
@[simp]
theorem local_homeomorph.restr_apply {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
(e.restr s) = e
@[simp]
theorem local_homeomorph.restr_symm_apply {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
((e.restr s).symm) = (e.symm)
@[simp]
theorem local_homeomorph.restr_to_local_equiv {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
theorem local_homeomorph.restr_source' {α : Type u_1} {β : Type u_2} (e : β) (s : set α) (hs : is_open s) :
theorem local_homeomorph.restr_to_local_equiv' {α : Type u_1} {β : Type u_2} (e : β) (s : set α) (hs : is_open s) :
theorem local_homeomorph.restr_eq_of_source_subset {α : Type u_1} {β : Type u_2} {e : β} {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} {e : β} :
= e
theorem local_homeomorph.restr_source_inter {α : Type u_1} {β : Type u_2} (e : β) (s : set α) :
theorem local_homeomorph.refl_source (α : Type u_1)  :
@[simp]
theorem local_homeomorph.refl_apply (α : Type u_1)  :
@[protected]
def local_homeomorph.refl (α : Type u_1)  :

The identity on the whole space as a local homeomorphism.

Equations
theorem local_homeomorph.refl_target (α : Type u_1)  :
@[simp]
theorem local_homeomorph.refl_local_equiv {α : Type u_1}  :
@[simp]
theorem local_homeomorph.refl_symm {α : Type u_1}  :
def local_homeomorph.of_set {α : Type u_1} (s : set α) (hs : is_open s) :

The identity local equiv on a set `s`

Equations
@[simp]
theorem local_homeomorph.of_set_apply {α : Type u_1} (s : set α) (hs : is_open s) :
theorem local_homeomorph.of_set_source {α : Type u_1} (s : set α) (hs : is_open s) :
theorem local_homeomorph.of_set_target {α : Type u_1} (s : set α) (hs : is_open s) :
@[simp]
theorem local_homeomorph.of_set_to_local_equiv {α : Type u_1} {s : set α} (hs : is_open s) :
@[simp]
theorem local_homeomorph.of_set_symm {α : Type u_1} {s : set α} (hs : is_open s) :
hs).symm =
@[simp]
theorem local_homeomorph.of_set_univ_eq_refl {α : Type u_1}  :
@[protected]
def local_homeomorph.trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) (h : e.to_local_equiv.target = e'.to_local_equiv.source) :

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} (e : β) (e' : γ) :

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

Equations
@[simp]
theorem local_homeomorph.trans_to_local_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
@[simp]
theorem local_homeomorph.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
(e.trans e') = e' e
@[simp]
theorem local_homeomorph.coe_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
((e.trans e').symm) = (e.symm) (e'.symm)
theorem local_homeomorph.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) {x : α} :
(e.trans e') x = e' (e x)
theorem local_homeomorph.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
theorem local_homeomorph.trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_homeomorph.trans_source' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_homeomorph.trans_source'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_homeomorph.image_trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_homeomorph.trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_homeomorph.trans_target' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_homeomorph.trans_target'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_homeomorph.inv_image_trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : γ) :
theorem local_homeomorph.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_homeomorph.trans_refl {α : Type u_1} {β : Type u_2} (e : β) :
= e
@[simp]
theorem local_homeomorph.refl_trans {α : Type u_1} {β : Type u_2} (e : β) :
= e
theorem local_homeomorph.trans_of_set {α : Type u_1} {β : Type u_2} (e : β) {s : set β} (hs : is_open s) :
e.trans hs) = e.restr (e ⁻¹' s)
theorem local_homeomorph.trans_of_set' {α : Type u_1} {β : Type u_2} (e : β) {s : set β} (hs : is_open s) :
theorem local_homeomorph.of_set_trans {α : Type u_1} {β : Type u_2} (e : β) {s : set α} (hs : is_open s) :
hs).trans e = e.restr s
theorem local_homeomorph.of_set_trans' {α : Type u_1} {β : Type u_2} (e : β) {s : set α} (hs : is_open s) :
@[simp]
theorem local_homeomorph.of_set_trans_of_set {α : Type u_1} {s : set α} (hs : is_open s) {s' : set α} (hs' : is_open s') :
hs).trans hs') = local_homeomorph.of_set (s s') _
theorem local_homeomorph.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
def local_homeomorph.trans_homeomorph {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (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_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β ≃ₜ γ) :
@[simp]
theorem local_homeomorph.trans_homeomorph_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β ≃ₜ γ) :
@[simp]
theorem local_homeomorph.trans_homeomorph_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β ≃ₜ γ) :
@[simp]
theorem local_homeomorph.trans_homeomorph_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β ≃ₜ γ) :
theorem local_homeomorph.trans_equiv_eq_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) (e' : β ≃ₜ γ) :
@[simp]
theorem homeomorph.trans_local_homeomorph_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α ≃ₜ β) :
def homeomorph.trans_local_homeomorph {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α ≃ₜ β) :

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

Equations
@[simp]
theorem homeomorph.trans_local_homeomorph_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α ≃ₜ β) :
@[simp]
theorem homeomorph.trans_local_homeomorph_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α ≃ₜ β) :
= e' e
@[simp]
theorem homeomorph.trans_local_homeomorph_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α ≃ₜ β) :
theorem homeomorph.trans_local_homeomorph_eq_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e' : γ) (e : α ≃ₜ β) :
def local_homeomorph.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. They should really be considered the same local equiv.

Equations
theorem local_homeomorph.eq_on_source_iff {α : Type u_1} {β : Type u_2} (e e' : β) :
@[protected, instance]
def local_homeomorph.setoid {α : Type u_1} {β : Type u_2}  :
setoid β)

`eq_on_source` is an equivalence relation

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

If two local homeomorphisms are equivalent, so are their inverses

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

Two equivalent local homeomorphisms have the same source

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

Two equivalent local homeomorphisms have the same target

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

Two equivalent local homeomorphisms have coinciding `to_fun` on the source

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

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} {e e' : β} {f f' : γ} (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} {e e' : β} (he : e e') (s : set α) :
e.restr s e'.restr s

Restriction of local homeomorphisms respects equivalence

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

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

theorem local_homeomorph.trans_symm_self {α : Type u_1} {β : Type u_2} (e : β) :
theorem local_homeomorph.eq_of_eq_on_source_univ {α : Type u_1} {β : Type u_2} {e e' : β} (h : e e') (s : e.to_local_equiv.source = set.univ) (t : e.to_local_equiv.target = set.univ) :
e = e'
@[simp]
theorem local_homeomorph.prod_to_local_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : δ) :
theorem local_homeomorph.prod_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : δ) :
@[simp]
theorem local_homeomorph.prod_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : δ) :
(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} (e : β) (e' : δ) :
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} (e : β) (e' : δ) (p : β × δ) :
((e.prod e').symm) p = ((e.symm) p.fst, (e'.symm) p.snd)
theorem local_homeomorph.prod_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : β) (e' : δ) :
@[simp]
theorem local_homeomorph.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_homeomorph.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')
theorem local_homeomorph.prod_eq_prod_of_nonempty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {e₁ e₁' : β} {e₂ e₂' : δ} (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} {e₁ e₁' : β} {e₂ e₂' : δ} (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} (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) (Hs : = ) (Heq : e' ) :
(e.piecewise e' s t H H' Hs Heq).to_local_equiv = t H H'
def local_homeomorph.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) (Hs : = ) (Heq : e' ) :

Combine two `local_homeomorph`s 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} (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) (Hs : = ) (Heq : e' ) :
(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} (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) (Hs : = ) (Heq : e' ) :
(e.piecewise e' s t H H' Hs Heq).symm = e.symm.piecewise e'.symm t s _ _ _ _
def local_homeomorph.disjoint_union {α : Type u_1} {β : Type u_2} (e e' : β) [Π (x : α), decidable (x e.to_local_equiv.source)] [Π (y : β), decidable (y e.to_local_equiv.target)] (Hs : e'.to_local_equiv.source) (Ht : e'.to_local_equiv.target) :

Combine two `local_homeomorph`s 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_homeomorph`s.

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)) :
= local_equiv.pi (λ (i : ι), (ei i).to_local_equiv)
theorem local_homeomorph.continuous_within_at_iff_continuous_within_at_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) {f : β → γ} {s : set β} {x : β} (h : x e.to_local_equiv.target) :

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} (e : β) {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

theorem local_homeomorph.continuous_on_iff_continuous_on_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) {f : β → γ} {s : set β} (h : s e.to_local_equiv.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.

theorem local_homeomorph.continuous_within_at_iff_continuous_within_at_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) {f : γ → α} {s : set γ} {x : γ} (hx : f x e.to_local_equiv.source) (h : s) :

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

theorem local_homeomorph.continuous_at_iff_continuous_at_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) {f : γ → α} {x : γ} (h : nhds x) :

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

theorem local_homeomorph.continuous_on_iff_continuous_on_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) {f : γ → α} {s : set γ} (h : s ) :

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.

theorem local_homeomorph.continuous_iff_continuous_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β) {f : γ → α} (h : = set.univ) :

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.to_homeomorph_source_target {α : Type u_1} {β : Type u_2} (e : β) :

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

Equations
theorem local_homeomorph.second_countable_topology_source {α : Type u_1} {β : Type u_2} (e : β) :

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
theorem local_homeomorph.to_open_embedding {α : Type u_1} {β : Type u_2} (e : β) (h : e.to_local_equiv.source = set.univ) :

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`.

@[simp]
theorem homeomorph.refl_to_local_homeomorph {α : Type u_1}  :
@[simp]
theorem homeomorph.symm_to_local_homeomorph {α : Type u_1} {β : Type u_2} (e : α ≃ₜ β) :
@[simp]
theorem homeomorph.trans_to_local_homeomorph {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ₜ β) (e' : β ≃ₜ γ) :
noncomputable def open_embedding.to_local_homeomorph {α : Type u_1} {β : Type u_2} (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
@[simp]
theorem open_embedding.to_local_homeomorph_apply {α : Type u_1} {β : Type u_2} (f : α → β) (h : open_embedding f) [nonempty α] :
@[simp]
theorem open_embedding.to_local_homeomorph_source {α : Type u_1} {β : Type u_2} (f : α → β) (h : open_embedding f) [nonempty α] :
@[simp]
theorem open_embedding.to_local_homeomorph_target {α : Type u_1} {β : Type u_2} (f : α → β) (h : open_embedding f) [nonempty α] :
theorem open_embedding.continuous_at_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} (hf : open_embedding f) {x : α} :
continuous_at (g f) x (f x)

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

Equations
noncomputable def local_homeomorph.subtype_restr {α : Type u_1} {β : Type u_2} (e : β) (s : topological_space.opens α) [nonempty s] :

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
theorem local_homeomorph.subtype_restr_def {α : Type u_1} {β : Type u_2} (e : β) (s : topological_space.opens α) [nonempty s] :
@[simp]
theorem local_homeomorph.subtype_restr_coe {α : Type u_1} {β : Type u_2} (e : β) (s : topological_space.opens α) [nonempty s] :
@[simp]
theorem local_homeomorph.subtype_restr_source {α : Type u_1} {β : Type u_2} (e : β) (s : topological_space.opens α) [nonempty s] :