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)
- to_local_equiv : local_equiv α β
- open_source : is_open c.to_local_equiv.source
- open_target : is_open c.to_local_equiv.target
- continuous_to_fun : continuous_on c.to_local_equiv.to_fun c.to_local_equiv.source
- continuous_inv_fun : continuous_on c.to_local_equiv.inv_fun c.to_local_equiv.target
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
- e.to_local_homeomorph = {to_local_equiv := {to_fun := e.to_equiv.to_local_equiv.to_fun, inv_fun := e.to_equiv.to_local_equiv.inv_fun, source := e.to_equiv.to_local_equiv.source, target := e.to_equiv.to_local_equiv.target, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
@[instance]
def
local_homeomorph.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
Equations
- local_homeomorph.has_coe_to_fun = {F := λ (e : local_homeomorph α β), α → β, coe := λ (e : local_homeomorph α β), e.to_local_equiv.to_fun}
def
local_homeomorph.symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
local_homeomorph α β → local_homeomorph β α
The inverse of a local homeomorphism
Equations
- e.symm = {to_local_equiv := {to_fun := e.to_local_equiv.symm.to_fun, inv_fun := e.to_local_equiv.symm.inv_fun, source := e.to_local_equiv.symm.source, target := e.to_local_equiv.symm.target, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
theorem
local_homeomorph.continuous_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
theorem
local_homeomorph.continuous_on_symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
@[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) :
⇑{to_local_equiv := e, open_source := a, open_target := b, continuous_to_fun := c, continuous_inv_fun := d} = ⇑e
@[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) :
⇑({to_local_equiv := e, open_source := a, open_target := b, continuous_to_fun := c, continuous_inv_fun := d}.symm) = ⇑(e.symm)
@[simp]
theorem
local_homeomorph.to_fun_eq_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
e.to_local_equiv.to_fun = ⇑e
@[simp]
theorem
local_homeomorph.inv_fun_eq_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
e.to_local_equiv.inv_fun = ⇑(e.symm)
@[simp]
theorem
local_homeomorph.coe_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
⇑(e.to_local_equiv) = ⇑e
@[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 : α} :
x ∈ e.to_local_equiv.source → ⇑e x ∈ e.to_local_equiv.target
@[simp]
theorem
local_homeomorph.map_target
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : β} :
x ∈ e.to_local_equiv.target → ⇑(e.symm) x ∈ e.to_local_equiv.source
@[simp]
theorem
local_homeomorph.left_inv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α} :
@[simp]
theorem
local_homeomorph.right_inv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : β} :
theorem
local_homeomorph.source_preimage_target
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
theorem
local_homeomorph.eq_of_local_equiv_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e e' : local_homeomorph α β} :
e.to_local_equiv = e'.to_local_equiv → e = e'
theorem
local_homeomorph.eventually_left_inverse
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α} :
theorem
local_homeomorph.eventually_left_inverse'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : β} :
theorem
local_homeomorph.eventually_right_inverse
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : β} :
theorem
local_homeomorph.eventually_right_inverse'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α} :
theorem
local_homeomorph.image_eq_target_inter_inv_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{s : set α} :
theorem
local_homeomorph.image_inter_source_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α) :
⇑e '' (s ∩ e.to_local_equiv.source) = e.to_local_equiv.target ∩ ⇑(e.symm) ⁻¹' (s ∩ e.to_local_equiv.source)
theorem
local_homeomorph.symm_image_eq_source_inter_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{s : set β} :
theorem
local_homeomorph.symm_image_inter_target_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set β) :
⇑(e.symm) '' (s ∩ e.to_local_equiv.target) = e.to_local_equiv.source ∩ ⇑e ⁻¹' (s ∩ e.to_local_equiv.target)
@[ext]
theorem
local_homeomorph.ext
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e e' : local_homeomorph α β) :
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]
theorem
local_homeomorph.symm_to_local_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
theorem
local_homeomorph.symm_source
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
theorem
local_homeomorph.symm_target
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
@[simp]
theorem
local_homeomorph.symm_symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
theorem
local_homeomorph.continuous_at
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α} :
x ∈ e.to_local_equiv.source → continuous_at ⇑e 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 : β} :
x ∈ e.to_local_equiv.target → continuous_at ⇑(e.symm) 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 : α} :
x ∈ e.to_local_equiv.source → filter.tendsto ⇑(e.symm) (nhds (⇑e x)) (nhds x)
theorem
local_homeomorph.preimage_interior
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set β) :
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 α) :
is_open s → local_homeomorph α β
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
- e.restr_open s hs = {to_local_equiv := {to_fun := (e.to_local_equiv.restr s).to_fun, inv_fun := (e.to_local_equiv.restr s).inv_fun, source := (e.to_local_equiv.restr s).source, target := (e.to_local_equiv.restr s).target, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
@[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) :
(e.restr_open s hs).to_local_equiv = e.to_local_equiv.restr 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) :
(e.restr_open s hs).to_local_equiv.source = e.to_local_equiv.source ∩ 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
- e.restr s = e.restr_open (interior s) is_open_interior
@[simp]
theorem
local_homeomorph.restr_to_local_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α) :
(e.restr s).to_local_equiv = e.to_local_equiv.restr (interior s)
@[simp]
theorem
local_homeomorph.restr_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α) :
@[simp]
theorem
local_homeomorph.restr_coe_symm
{α : 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 α) :
(e.restr s).to_local_equiv.source = e.to_local_equiv.source ∩ interior s
theorem
local_homeomorph.restr_target
{α : 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 α) :
is_open s → (e.restr s).to_local_equiv.source = e.to_local_equiv.source ∩ s
theorem
local_homeomorph.restr_to_local_equiv'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α) :
is_open s → (e.restr s).to_local_equiv = e.to_local_equiv.restr s
theorem
local_homeomorph.restr_eq_of_source_subset
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α} :
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 α) :
The identity on the whole space as a local homeomorphism.
Equations
@[simp]
@[simp]
@[simp]
def
local_homeomorph.of_set
{α : Type u_1}
[topological_space α]
(s : set α) :
is_open s → local_homeomorph α α
The identity local equiv on a set s
Equations
- local_homeomorph.of_set s hs = {to_local_equiv := {to_fun := (local_equiv.of_set s).to_fun, inv_fun := (local_equiv.of_set s).inv_fun, source := (local_equiv.of_set s).source, target := (local_equiv.of_set s).target, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := hs, open_target := hs, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
local_homeomorph.of_set_to_local_equiv
{α : Type u_1}
[topological_space α]
{s : set α}
(hs : is_open s) :
theorem
local_homeomorph.of_set_source
{α : Type u_1}
[topological_space α]
{s : set α}
(hs : is_open s) :
(local_homeomorph.of_set s hs).to_local_equiv.source = s
theorem
local_homeomorph.of_set_target
{α : Type u_1}
[topological_space α]
{s : set α}
(hs : is_open s) :
(local_homeomorph.of_set s hs).to_local_equiv.target = s
@[simp]
theorem
local_homeomorph.of_set_coe
{α : Type u_1}
[topological_space α]
{s : set α}
(hs : is_open s) :
⇑(local_homeomorph.of_set s hs) = id
@[simp]
theorem
local_homeomorph.of_set_symm
{α : Type u_1}
[topological_space α]
{s : set α}
(hs : is_open s) :
(local_homeomorph.of_set s hs).symm = local_homeomorph.of_set s hs
@[simp]
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 β γ) :
e.to_local_equiv.target = e'.to_local_equiv.source → local_homeomorph α γ
Composition of two local homeomorphisms when the target of the first and the source of the second coincide.
Equations
- e.trans' e' h = {to_local_equiv := {to_fun := (e.to_local_equiv.trans' e'.to_local_equiv h).to_fun, inv_fun := (e.to_local_equiv.trans' e'.to_local_equiv h).inv_fun, source := (e.to_local_equiv.trans' e'.to_local_equiv h).source, target := (e.to_local_equiv.trans' e'.to_local_equiv h).target, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
def
local_homeomorph.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ] :
local_homeomorph α β → local_homeomorph β γ → local_homeomorph α γ
Composing two local homeomorphisms, by restricting to the maximal domain where their composition is well defined.
Equations
- e.trans e' = (e.symm.restr_open e'.to_local_equiv.source _).symm.trans' (e'.restr_open e.to_local_equiv.target _) _
@[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 β γ) :
(e.trans e').to_local_equiv = e.to_local_equiv.trans e'.to_local_equiv
@[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 β γ) :
@[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 β γ) :
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 β γ) :
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 β γ) :
(e.trans e').to_local_equiv.source = e.to_local_equiv.source ∩ ⇑e ⁻¹' e'.to_local_equiv.source
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 β γ) :
(e.trans e').to_local_equiv.source = e.to_local_equiv.source ∩ ⇑e ⁻¹' (e.to_local_equiv.target ∩ e'.to_local_equiv.source)
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 β γ) :
(e.trans e').to_local_equiv.source = ⇑(e.symm) '' (e.to_local_equiv.target ∩ e'.to_local_equiv.source)
theorem
local_homeomorph.image_trans_source
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : local_homeomorph β γ) :
⇑e '' (e.trans e').to_local_equiv.source = e.to_local_equiv.target ∩ e'.to_local_equiv.source
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 β γ) :
(e.trans e').to_local_equiv.target = e'.to_local_equiv.target ∩ ⇑(e'.symm) ⁻¹' e.to_local_equiv.target
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 β γ) :
(e.trans e').to_local_equiv.target = e'.to_local_equiv.target ∩ ⇑(e'.symm) ⁻¹' (e'.to_local_equiv.source ∩ e.to_local_equiv.target)
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 β γ) :
(e.trans e').to_local_equiv.target = ⇑e' '' (e'.to_local_equiv.source ∩ e.to_local_equiv.target)
theorem
local_homeomorph.inv_image_trans_target
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : local_homeomorph β γ) :
⇑(e'.symm) '' (e.trans e').to_local_equiv.target = e'.to_local_equiv.source ∩ e.to_local_equiv.target
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 γ δ) :
@[simp]
theorem
local_homeomorph.trans_refl
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
e.trans (local_homeomorph.refl β) = e
@[simp]
theorem
local_homeomorph.refl_trans
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
(local_homeomorph.refl α).trans e = e
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) :
e.trans (local_homeomorph.of_set s hs) = e.restr (e.to_local_equiv.source ∩ ⇑e ⁻¹' 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) :
(local_homeomorph.of_set s hs).trans e = e.restr 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) :
(local_homeomorph.of_set s hs).trans e = e.restr (e.to_local_equiv.source ∩ 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') :
(local_homeomorph.of_set s hs).trans (local_homeomorph.of_set s' hs') = local_homeomorph.of_set (s ∩ 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 α) :
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
- e.eq_on_source e' = (e.to_local_equiv.source = e'.to_local_equiv.source ∧ set.eq_on ⇑e ⇑e' e.to_local_equiv.source)
theorem
local_homeomorph.eq_on_source_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e e' : local_homeomorph α β) :
e.eq_on_source e' ↔ e.to_local_equiv.eq_on_source e'.to_local_equiv
@[instance]
def
local_homeomorph.setoid
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
setoid (local_homeomorph α β)
eq_on_source is an equivalence relation
Equations
- local_homeomorph.setoid = {r := local_homeomorph.eq_on_source _inst_2, iseqv := _}
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 α β} :
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 α β} :
e ≈ e' → e.to_local_equiv.source = e'.to_local_equiv.source
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 α β} :
e ≈ e' → e.to_local_equiv.target = e'.to_local_equiv.target
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 β γ} :
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 α) :
Restriction of local homeomorphisms respects equivalence
theorem
local_homeomorph.trans_self_symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
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}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
theorem
local_homeomorph.eq_of_eq_on_source_univ
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e e' : local_homeomorph α β} :
e ≈ e' → e.to_local_equiv.source = set.univ → e.to_local_equiv.target = set.univ → e = e'
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
- e.prod e' = {to_local_equiv := {to_fun := (e.to_local_equiv.prod e'.to_local_equiv).to_fun, inv_fun := (e.to_local_equiv.prod e'.to_local_equiv).inv_fun, source := (e.to_local_equiv.prod e'.to_local_equiv).source, target := (e.to_local_equiv.prod e'.to_local_equiv).target, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
@[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 γ δ) :
(e.prod e').to_local_equiv = e.to_local_equiv.prod e'.to_local_equiv
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 γ δ) :
(e.prod e').to_local_equiv.source = e.to_local_equiv.source.prod e'.to_local_equiv.source
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 γ δ) :
(e.prod e').to_local_equiv.target = e.to_local_equiv.target.prod e'.to_local_equiv.target
@[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 γ δ) :
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 γ δ) :
@[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 γ δ) :
@[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 η ε) :
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 : β} :
x ∈ e.to_local_equiv.target → (continuous_within_at f s x ↔ continuous_within_at (f ∘ ⇑e) (⇑e ⁻¹' s) (⇑(e.symm) 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 : β} :
x ∈ e.to_local_equiv.target → (continuous_at f x ↔ continuous_at (f ∘ ⇑e) (⇑(e.symm) 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 β} :
s ⊆ e.to_local_equiv.target → (continuous_on f s ↔ continuous_on (f ∘ ⇑e) (e.to_local_equiv.source ∩ ⇑e ⁻¹' s))
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 : γ} :
f x ∈ e.to_local_equiv.source → f ⁻¹' e.to_local_equiv.source ∈ nhds_within x s → (continuous_within_at f s x ↔ continuous_within_at (⇑e ∘ f) s 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 : γ} :
f ⁻¹' e.to_local_equiv.source ∈ nhds x → (continuous_at f x ↔ continuous_at (⇑e ∘ 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 γ} :
s ⊆ f ⁻¹' e.to_local_equiv.source → (continuous_on f s ↔ continuous_on (⇑e ∘ f) 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.
def
local_homeomorph.to_homeomorph_of_source_eq_univ_target_eq_univ
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
e.to_local_equiv.source = set.univ → e.to_local_equiv.target = set.univ → α ≃ₜ β
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
- e.to_homeomorph_of_source_eq_univ_target_eq_univ h h' = {to_equiv := {to_fun := ⇑e, inv_fun := ⇑(e.symm), left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
local_homeomorph.to_homeomorph_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(h : e.to_local_equiv.source = set.univ)
(h' : e.to_local_equiv.target = set.univ) :
@[simp]
theorem
local_homeomorph.to_homeomorph_symm_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(h : e.to_local_equiv.source = set.univ)
(h' : e.to_local_equiv.target = set.univ) :
theorem
local_homeomorph.to_open_embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
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_source
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
@[simp]
theorem
homeomorph.to_local_homeomorph_target
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
@[simp]
theorem
homeomorph.to_local_homeomorph_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
⇑(e.to_local_homeomorph) = ⇑e
@[simp]
theorem
homeomorph.to_local_homeomorph_coe_symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
@[simp]
@[simp]
theorem
homeomorph.symm_to_local_homeomorph
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
@[simp]
theorem
homeomorph.trans_to_local_homeomorph
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : α ≃ₜ β)
(e' : β ≃ₜ γ) :
(e.trans e').to_local_homeomorph = e.to_local_homeomorph.trans e'.to_local_homeomorph
def
open_embedding.to_local_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[nonempty α]
{f : α → β} :
open_embedding f → local_equiv α β
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) :
⇑(h.to_local_equiv) = 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) :
theorem
open_embedding.continuous_inv_fun
{α : 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 : α → β} :
open_embedding f → local_homeomorph α β
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
- h.to_local_homeomorph = {to_local_equiv := h.to_local_equiv, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
open_embedding.to_local_homeomorph_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[nonempty α]
{f : α → β}
(h : open_embedding f) :
⇑(h.to_local_homeomorph) = 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 : α} :
continuous_at (g ∘ f) x ↔ continuous_at g (f x)
def
topological_space.opens.local_homeomorph_subtype_coe
{α : Type u_1}
[topological_space α]
(s : topological_space.opens α)
[nonempty ↥s] :
The inclusion of an open subset s of a space α into α is a local homeomorphism from the
subtype s to α.
Equations
@[simp]
theorem
topological_space.opens.local_homeomorph_subtype_coe_coe
{α : Type u_1}
[topological_space α]
(s : topological_space.opens α)
[nonempty ↥s] :
@[simp]
theorem
topological_space.opens.local_homeomorph_subtype_coe_source
{α : Type u_1}
[topological_space α]
(s : topological_space.opens α)
[nonempty ↥s] :
@[simp]
theorem
topological_space.opens.local_homeomorph_subtype_coe_target
{α : Type u_1}
[topological_space α]
(s : topological_space.opens α)
[nonempty ↥s] :
def
local_homeomorph.subtype_restr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(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}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : topological_space.opens α)
[nonempty ↥s] :
@[simp]
theorem
local_homeomorph.subtype_restr_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : topological_space.opens α)
[nonempty ↥s] :
⇑(e.subtype_restr s) = set.restrict ⇑e ↑s
@[simp]
theorem
local_homeomorph.subtype_restr_source
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : topological_space.opens α)
[nonempty ↥s] :
(e.subtype_restr s).to_local_equiv.source = coe ⁻¹' e.to_local_equiv.source
theorem
local_homeomorph.subtype_restr_symm_trans_subtype_restr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(s : topological_space.opens α)
[nonempty ↥s]
(f f' : local_homeomorph α β) :
(f.subtype_restr s).symm.trans (f'.subtype_restr s) ≈ (f.symm.trans f').restr (f.to_local_equiv.target ∩ ⇑(f.symm) ⁻¹' ↑s)