mathlib documentation

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.

@[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

def homeomorph.to_local_homeomorph {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
α ≃ₜ βlocal_homeomorph α β

A homeomorphism induces a local homeomorphism on the whole space

Equations
@[instance]

Equations
def local_homeomorph.symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

The inverse of a local homeomorphism

Equations
@[simp]
theorem local_homeomorph.mk_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_equiv α β) (a : is_open e.source) (b : is_open e.target) (c : continuous_on e.to_fun e.source) (d : continuous_on e.inv_fun e.target) :

@[simp]
theorem local_homeomorph.mk_coe_symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_equiv α β) (a : is_open e.source) (b : is_open e.target) (c : continuous_on e.to_fun e.source) (d : continuous_on e.inv_fun e.target) :

@[simp]
theorem local_homeomorph.to_fun_eq_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :

@[simp]
theorem local_homeomorph.inv_fun_eq_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :

@[simp]
theorem local_homeomorph.coe_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :

@[simp]
theorem local_homeomorph.coe_coe_symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :

@[simp]
theorem local_homeomorph.map_source {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} :

@[simp]
theorem local_homeomorph.map_target {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : β} :

@[simp]
theorem local_homeomorph.left_inv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} :
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 : β} :
x e.to_local_equiv.targete ((e.symm) x) = x

theorem local_homeomorph.eq_of_local_equiv_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e e' : local_homeomorph α β} :

theorem local_homeomorph.eventually_left_inverse {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} :
x e.to_local_equiv.source(∀ᶠ (y : α) in 𝓝 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 : β} :
x e.to_local_equiv.target(∀ᶠ (y : α) in 𝓝 ((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 : β} :
x e.to_local_equiv.target(∀ᶠ (y : β) in 𝓝 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 : α} :
x e.to_local_equiv.source(∀ᶠ (y : β) in 𝓝 (e x), e ((e.symm) y) = y)

@[ext]
theorem local_homeomorph.ext {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e e' : local_homeomorph α β) :
(∀ (x : α), e x = e' x)(∀ (x : β), (e.symm) x = (e'.symm) x)e.to_local_equiv.source = e'.to_local_equiv.sourcee = 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.

@[simp]

@[simp]
theorem local_homeomorph.symm_symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :
e.symm.symm = e

theorem local_homeomorph.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {x : α} :

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 : β} :

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 : α} :

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

theorem local_homeomorph.preimage_open_of_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {s : set β} :

theorem local_homeomorph.preimage_open_of_open_symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) {s : set α} :

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

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 α} :

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

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

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} [topological_space α] [topological_space β] (e : local_homeomorph α β) (s : set α) (hs : is_open s) :

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

def local_homeomorph.restr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
local_homeomorph α βset αlocal_homeomorph α β

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_to_local_equiv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) (s : set α) :

@[simp]
theorem local_homeomorph.restr_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) (s : set α) :
(e.restr s) = e

@[simp]
theorem local_homeomorph.restr_coe_symm {α : 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_source {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) (s : set α) :

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

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

theorem local_homeomorph.restr_eq_of_source_subset {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : local_homeomorph α β} {s : set α} :

@[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 α) :

def local_homeomorph.refl (α : Type u_1) [topological_space α] :

The identity on the whole space as a local homeomorphism.

Equations
@[simp]

@[simp]
theorem local_homeomorph.of_set_coe {α : Type u_1} [topological_space α] {s : set α} (hs : is_open s) :

@[simp]
theorem local_homeomorph.of_set_symm {α : Type u_1} [topological_space α] {s : set α} (hs : is_open s) :

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 β γ) :

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

Equations
def local_homeomorph.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] :

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} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : local_homeomorph β γ) :

@[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 ≫ₕ 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 ≫ₕ e').symm) = (e.symm) (e'.symm)

theorem local_homeomorph.trans_symm_eq_symm_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : local_homeomorph β γ) :
(e ≫ₕ e').symm = e'.symm ≫ₕ e.symm

theorem local_homeomorph.trans_source'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : local_homeomorph β γ) :

theorem local_homeomorph.trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : local_homeomorph β γ) :

theorem local_homeomorph.trans_target'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) (e' : local_homeomorph β γ) :

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 ≫ₕ e') ≫ₕ e'' = e ≫ₕ e' ≫ₕ e''

@[simp]
theorem local_homeomorph.trans_refl {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :

@[simp]
theorem local_homeomorph.refl_trans {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : local_homeomorph α β) :

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.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) :

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 ≫ₕ e' = (e ≫ₕ e').restr s

def local_homeomorph.eq_on_source {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
local_homeomorph α β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
@[instance]
def local_homeomorph.setoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

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 α β} :
e e'e.symm e'.symm

If two local homeomorphisms are equivalent, so are their inverses

theorem local_homeomorph.eq_on_source.source_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e e' : local_homeomorph α β} :

Two equivalent local homeomorphisms have the same source

theorem local_homeomorph.eq_on_source.target_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e e' : local_homeomorph α β} :

Two equivalent local homeomorphisms have the same target

theorem local_homeomorph.eq_on_source.eq_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e e' : local_homeomorph α β} :

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} [topological_space α] [topological_space β] {e e' : local_homeomorph α β} :

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 β γ} :
e e'f f'e ≫ₕ f e' ≫ₕ 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

theorem local_homeomorph.eq_of_eq_on_source_univ {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e e' : local_homeomorph α β} :

def local_homeomorph.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] :
local_homeomorph α βlocal_homeomorph γ δlocal_homeomorph × γ) × δ)

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

Equations
@[simp]
theorem local_homeomorph.prod_to_local_equiv {α : 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 γ δ) :

theorem local_homeomorph.prod_source {α : 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 γ δ) :

theorem local_homeomorph.prod_target {α : 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 γ δ) :

@[simp]
theorem local_homeomorph.prod_coe {α : 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)

theorem local_homeomorph.prod_coe_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) = λ (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' ≫ₕ f.prod f' = (e ≫ₕ f).prod (e' ≫ₕ f')

theorem local_homeomorph.continuous_within_at_iff_continuous_within_at_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) {f : β → γ} {s : set β} {x : β} :

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 : β} :

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} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) {f : β → γ} {s : set β} :

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} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) {f : γ → α} {s : set γ} {x : γ} :

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} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) {f : γ → α} {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} [topological_space α] [topological_space β] [topological_space γ] (e : local_homeomorph α β) {f : γ → α} {s : set γ} :

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.

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.

@[simp]
theorem homeomorph.to_local_homeomorph_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : α ≃ₜ β) :

@[simp]
theorem homeomorph.to_local_homeomorph_coe_symm {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (e : α ≃ₜ β) :

@[simp]

@[simp]
theorem homeomorph.trans_to_local_homeomorph {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (e : α ≃ₜ β) (e' : β ≃ₜ γ) :

def open_embedding.to_local_equiv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [nonempty α] {f : α → β} :

An open embedding of α into β, with α nonempty, defines a local equivalence whose source is all of α. This is mainly an auxiliary lemma for the stronger result to_local_homeomorph.

Equations
@[simp]
theorem open_embedding.to_local_equiv_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [nonempty α] {f : α → β} (h : open_embedding f) :

@[simp]
theorem open_embedding.to_local_equiv_source {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [nonempty α] {f : α → β} (h : open_embedding f) :

@[simp]
theorem open_embedding.to_local_equiv_target {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [nonempty α] {f : α → β} (h : open_embedding f) :

theorem open_embedding.open_target {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [nonempty α] {f : α → β} (h : open_embedding f) :

def open_embedding.to_local_homeomorph {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [nonempty α] {f : α → β} :

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_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [nonempty α] {f : α → β} (h : open_embedding f) :

@[simp]
theorem open_embedding.source {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [nonempty α] {f : α → β} (h : open_embedding f) :

@[simp]
theorem open_embedding.target {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [nonempty α] {f : α → β} (h : open_embedding f) :

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
@[simp]