Local homeomorphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines homeomorphisms between open subsets of topological spaces. An element e of
local_homeomorph α β is an extension of local_equiv α β, i.e., it is a pair of functions
e.to_fun and e.inv_fun, inverse of each other on the sets e.source and e.target.
Additionally, we require that these sets are open, and that the functions are continuous on them.
Equivalently, they are homeomorphisms there.
As in equivs, we register a coercion to functions, and we use e x and e.symm x throughout
instead of e.to_fun x and e.inv_fun x.
Main definitions #
homeomorph.to_local_homeomorph: associating a local homeomorphism to a homeomorphism, with
source = target = univ
local_homeomorph.symm : the inverse of a local homeomorphism
local_homeomorph.trans : the composition of two local homeomorphisms
local_homeomorph.refl : the identity local homeomorphism
local_homeomorph.of_set: the identity on a set s
eq_on_source : equivalence relation describing the "right" notion of equality for local
homeomorphisms
Implementation notes #
Most statements are copied from their local_equiv versions, although some care is required especially when restricting to subsets, as these should be open subsets.
For design notes, see local_equiv.lean.
Local coding conventions #
If a lemma deals with the intersection of a set with either source or target of a local_equiv,
then it should use e.source ∩ s or e.target ∩ t, not s ∩ e.source or t ∩ e.target.
@[nolint]
structure
local_homeomorph
(α : Type u_5)
(β : Type u_6)
[topological_space α]
[topological_space β] :
Type (max u_5 u_6)
- to_local_equiv : local_equiv α β
- open_source : is_open self.to_local_equiv.source
- open_target : is_open self.to_local_equiv.target
- continuous_to_fun : continuous_on self.to_local_equiv.to_fun self.to_local_equiv.source
- continuous_inv_fun : continuous_on self.to_local_equiv.inv_fun self.to_local_equiv.target
local homeomorphisms, defined on open subsets of the space
Instances for local_homeomorph
- local_homeomorph.has_sizeof_inst
- local_homeomorph.has_coe_to_fun
- local_homeomorph.setoid
- structure_groupoid.has_mem
@[protected, instance]
def
local_homeomorph.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
has_coe_to_fun (local_homeomorph α β) (λ (_x : local_homeomorph α β), α → β)
Equations
- local_homeomorph.has_coe_to_fun = {coe := λ (e : local_homeomorph α β), e.to_local_equiv.to_fun}
@[protected]
def
local_homeomorph.symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : 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 := _}
def
local_homeomorph.simps.apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
α → β
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
def
local_homeomorph.simps.symm_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
β → α
See Note [custom simps projection]
Equations
@[protected]
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)
theorem
local_homeomorph.to_local_equiv_injective
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
@[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 : α}
(h : 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 : β}
(h : 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 : α}
(h : x ∈ e.to_local_equiv.source) :
@[simp]
theorem
local_homeomorph.right_inv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : β}
(h : x ∈ e.to_local_equiv.target) :
theorem
local_homeomorph.eq_symm_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
{y : β}
(hx : x ∈ e.to_local_equiv.source)
(hy : y ∈ e.to_local_equiv.target) :
@[protected]
theorem
local_homeomorph.maps_to
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
@[protected]
theorem
local_homeomorph.symm_maps_to
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
@[protected]
theorem
local_homeomorph.left_inv_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
set.left_inv_on ⇑(e.symm) ⇑e e.to_local_equiv.source
@[protected]
theorem
local_homeomorph.right_inv_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
set.right_inv_on ⇑(e.symm) ⇑e e.to_local_equiv.target
@[protected]
theorem
local_homeomorph.inv_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
set.inv_on ⇑(e.symm) ⇑e e.to_local_equiv.source e.to_local_equiv.target
@[protected]
theorem
local_homeomorph.inj_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
@[protected]
theorem
local_homeomorph.bij_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
@[protected]
theorem
local_homeomorph.surj_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
@[simp]
theorem
homeomorph.to_local_homeomorph_target
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
@[simp]
theorem
homeomorph.to_local_homeomorph_symm_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
def
homeomorph.to_local_homeomorph
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
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 := _}
@[simp]
theorem
homeomorph.to_local_homeomorph_source
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
@[simp]
theorem
homeomorph.to_local_homeomorph_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : α ≃ₜ β) :
⇑(e.to_local_homeomorph) = ⇑e
def
local_homeomorph.replace_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(e' : local_equiv α β)
(h : e.to_local_equiv = e') :
local_homeomorph α β
Replace to_local_equiv field to provide better definitional equalities.
Equations
- e.replace_equiv e' h = {to_local_equiv := e', open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
theorem
local_homeomorph.replace_equiv_eq_self
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(e' : local_equiv α β)
(h : e.to_local_equiv = e') :
e.replace_equiv e' h = e
theorem
local_homeomorph.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 α β}
(h : 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 : α}
(hx : x ∈ e.to_local_equiv.source) :
theorem
local_homeomorph.eventually_left_inverse'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : β}
(hx : x ∈ e.to_local_equiv.target) :
theorem
local_homeomorph.eventually_right_inverse
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : β}
(hx : x ∈ e.to_local_equiv.target) :
theorem
local_homeomorph.eventually_right_inverse'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(hx : x ∈ e.to_local_equiv.source) :
theorem
local_homeomorph.eventually_ne_nhds_within
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(hx : x ∈ e.to_local_equiv.source) :
theorem
local_homeomorph.nhds_within_source_inter
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(hx : x ∈ e.to_local_equiv.source)
(s : set α) :
nhds_within x (e.to_local_equiv.source ∩ s) = nhds_within x s
theorem
local_homeomorph.nhds_within_target_inter
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : β}
(hx : x ∈ e.to_local_equiv.target)
(s : set β) :
nhds_within x (e.to_local_equiv.target ∩ s) = nhds_within x s
theorem
local_homeomorph.image_eq_target_inter_inv_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{s : set α}
(h : s ⊆ e.to_local_equiv.source) :
theorem
local_homeomorph.image_source_inter_eq'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α) :
theorem
local_homeomorph.image_source_inter_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α) :
⇑e '' (e.to_local_equiv.source ∩ s) = e.to_local_equiv.target ∩ ⇑(e.symm) ⁻¹' (e.to_local_equiv.source ∩ s)
theorem
local_homeomorph.symm_image_eq_source_inter_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{s : set β}
(h : s ⊆ e.to_local_equiv.target) :
theorem
local_homeomorph.symm_image_target_inter_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set β) :
⇑(e.symm) '' (e.to_local_equiv.target ∩ s) = e.to_local_equiv.source ∩ ⇑e ⁻¹' (e.to_local_equiv.target ∩ s)
theorem
local_homeomorph.source_inter_preimage_inv_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α) :
theorem
local_homeomorph.target_inter_inv_preimage_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set β) :
theorem
local_homeomorph.source_inter_preimage_target_inter
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set β) :
e.to_local_equiv.source ∩ ⇑e ⁻¹' (e.to_local_equiv.target ∩ s) = e.to_local_equiv.source ∩ ⇑e ⁻¹' s
theorem
local_homeomorph.image_source_eq_target
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
⇑e '' e.to_local_equiv.source = e.to_local_equiv.target
theorem
local_homeomorph.symm_image_target_eq_source
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
⇑(e.symm) '' e.to_local_equiv.target = e.to_local_equiv.source
@[protected, ext]
theorem
local_homeomorph.ext
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e e' : local_homeomorph α β)
(h : ∀ (x : α), ⇑e x = ⇑e' x)
(hinv : ∀ (x : β), ⇑(e.symm) x = ⇑(e'.symm) x)
(hs : e.to_local_equiv.source = e'.to_local_equiv.source) :
e = e'
Two local homeomorphisms are equal when they have equal to_fun, inv_fun and source.
It is not sufficient to have equal to_fun and source, as this only determines inv_fun on
the target. This would only be true for a weaker notion of equality, arguably the right one,
called eq_on_source.
@[protected]
theorem
local_homeomorph.ext_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e e' : local_homeomorph α β} :
@[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 α β) :
@[protected]
theorem
local_homeomorph.continuous_at
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(h : x ∈ e.to_local_equiv.source) :
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 : β}
(h : 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 : α}
(hx : x ∈ e.to_local_equiv.source) :
theorem
local_homeomorph.map_nhds_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(hx : x ∈ e.to_local_equiv.source) :
theorem
local_homeomorph.symm_map_nhds_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(hx : x ∈ e.to_local_equiv.source) :
theorem
local_homeomorph.image_mem_nhds
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(hx : x ∈ e.to_local_equiv.source)
{s : set α}
(hs : s ∈ nhds x) :
theorem
local_homeomorph.map_nhds_within_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(hx : x ∈ e.to_local_equiv.source)
(s : set α) :
filter.map ⇑e (nhds_within x s) = nhds_within (⇑e x) (⇑e '' (e.to_local_equiv.source ∩ s))
theorem
local_homeomorph.map_nhds_within_preimage_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(hx : x ∈ e.to_local_equiv.source)
(s : set β) :
filter.map ⇑e (nhds_within x (⇑e ⁻¹' s)) = nhds_within (⇑e x) s
theorem
local_homeomorph.eventually_nhds
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(p : β → Prop)
(hx : x ∈ e.to_local_equiv.source) :
theorem
local_homeomorph.eventually_nhds'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(p : α → Prop)
(hx : x ∈ e.to_local_equiv.source) :
theorem
local_homeomorph.eventually_nhds_within
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(p : β → Prop)
{s : set α}
(hx : x ∈ e.to_local_equiv.source) :
theorem
local_homeomorph.eventually_nhds_within'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{x : α}
(p : α → Prop)
{s : set α}
(hx : x ∈ e.to_local_equiv.source) :
theorem
local_homeomorph.preimage_eventually_eq_target_inter_preimage_inter
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{e : local_homeomorph α β}
{s : set α}
{t : set γ}
{x : α}
{f : α → γ}
(hf : continuous_within_at f s x)
(hxe : x ∈ e.to_local_equiv.source)
(ht : t ∈ nhds (f x)) :
This lemma is useful in the manifold library in the case that e is a chart. It states that
locally around e x the set e.symm ⁻¹' s is the same as the set intersected with the target
of e and some other neighborhood of f x (which will be the source of a chart on γ).
theorem
local_homeomorph.preimage_open_of_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{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}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α)
(t : set β) :
Prop
We say that t : set β is an image of s : set α under a local homeomorphism e if any of the
following equivalent conditions hold:
e '' (e.source ∩ s) = e.target ∩ t;e.source ∩ e ⁻¹ t = e.source ∩ s;∀ x ∈ e.source, e x ∈ t ↔ x ∈ s(this one is used in the definition).
theorem
local_homeomorph.is_image.to_local_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
e.to_local_equiv.is_image s t
theorem
local_homeomorph.is_image.apply_mem_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
{x : α}
(h : e.is_image s t)
(hx : x ∈ e.to_local_equiv.source) :
@[protected]
theorem
local_homeomorph.is_image.symm
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
theorem
local_homeomorph.is_image.symm_apply_mem_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
{y : β}
(h : e.is_image s t)
(hy : y ∈ e.to_local_equiv.target) :
@[simp]
theorem
local_homeomorph.is_image.symm_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β} :
@[protected]
theorem
local_homeomorph.is_image.maps_to
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
set.maps_to ⇑e (e.to_local_equiv.source ∩ s) (e.to_local_equiv.target ∩ t)
theorem
local_homeomorph.is_image.symm_maps_to
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
set.maps_to ⇑(e.symm) (e.to_local_equiv.target ∩ t) (e.to_local_equiv.source ∩ s)
theorem
local_homeomorph.is_image.image_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
⇑e '' (e.to_local_equiv.source ∩ s) = e.to_local_equiv.target ∩ t
theorem
local_homeomorph.is_image.symm_image_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
⇑(e.symm) '' (e.to_local_equiv.target ∩ t) = e.to_local_equiv.source ∩ s
theorem
local_homeomorph.is_image.iff_preimage_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β} :
theorem
local_homeomorph.is_image.preimage_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{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}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{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}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β} :
theorem
local_homeomorph.is_image.symm_preimage_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{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}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{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}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β} :
e.is_image s t ↔ e.to_local_equiv.target ∩ ⇑(e.symm) ⁻¹' (e.to_local_equiv.source ∩ s) = e.to_local_equiv.target ∩ t
theorem
local_homeomorph.is_image.of_symm_preimage_eq'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β} :
e.to_local_equiv.target ∩ ⇑(e.symm) ⁻¹' (e.to_local_equiv.source ∩ s) = e.to_local_equiv.target ∩ t → e.is_image s t
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}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β} :
e.is_image s t → e.to_local_equiv.target ∩ ⇑(e.symm) ⁻¹' (e.to_local_equiv.source ∩ s) = e.to_local_equiv.target ∩ t
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}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β} :
e.is_image s t ↔ e.to_local_equiv.source ∩ ⇑e ⁻¹' (e.to_local_equiv.target ∩ t) = e.to_local_equiv.source ∩ s
theorem
local_homeomorph.is_image.preimage_eq'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β} :
e.is_image s t → e.to_local_equiv.source ∩ ⇑e ⁻¹' (e.to_local_equiv.target ∩ t) = e.to_local_equiv.source ∩ s
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}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β} :
e.to_local_equiv.source ∩ ⇑e ⁻¹' (e.to_local_equiv.target ∩ t) = e.to_local_equiv.source ∩ s → e.is_image s t
Alias of the reverse direction of local_homeomorph.is_image.iff_preimage_eq'.
theorem
local_homeomorph.is_image.of_image_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : ⇑e '' (e.to_local_equiv.source ∩ s) = e.to_local_equiv.target ∩ t) :
e.is_image s t
theorem
local_homeomorph.is_image.of_symm_image_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : ⇑(e.symm) '' (e.to_local_equiv.target ∩ t) = e.to_local_equiv.source ∩ s) :
e.is_image s t
@[protected]
theorem
local_homeomorph.is_image.compl
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
@[protected]
theorem
local_homeomorph.is_image.inter
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
{s' : set α}
{t' : set β}
(h : e.is_image s t)
(h' : e.is_image s' t') :
@[protected]
theorem
local_homeomorph.is_image.union
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
{s' : set α}
{t' : set β}
(h : e.is_image s t)
(h' : e.is_image s' t') :
@[protected]
theorem
local_homeomorph.is_image.diff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
{s' : set α}
{t' : set β}
(h : e.is_image s t)
(h' : e.is_image s' t') :
theorem
local_homeomorph.is_image.left_inv_on_piecewise
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
{e' : local_homeomorph α β}
[Π (i : α), decidable (i ∈ s)]
[Π (i : β), decidable (i ∈ t)]
(h : e.is_image s t)
(h' : e'.is_image s t) :
set.left_inv_on (t.piecewise ⇑(e.symm) ⇑(e'.symm)) (s.piecewise ⇑e ⇑e') (s.ite e.to_local_equiv.source e'.to_local_equiv.source)
theorem
local_homeomorph.is_image.inter_eq_of_inter_eq_of_eq_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
{e' : local_homeomorph α β}
(h : e.is_image s t)
(h' : e'.is_image s t)
(hs : e.to_local_equiv.source ∩ s = e'.to_local_equiv.source ∩ s)
(Heq : set.eq_on ⇑e ⇑e' (e.to_local_equiv.source ∩ s)) :
e.to_local_equiv.target ∩ t = e'.to_local_equiv.target ∩ t
theorem
local_homeomorph.is_image.symm_eq_on_of_inter_eq_of_eq_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
{e' : local_homeomorph α β}
(h : e.is_image s t)
(hs : e.to_local_equiv.source ∩ s = e'.to_local_equiv.source ∩ s)
(Heq : set.eq_on ⇑e ⇑e' (e.to_local_equiv.source ∩ s)) :
theorem
local_homeomorph.is_image.map_nhds_within_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
{x : α}
(h : e.is_image s t)
(hx : x ∈ e.to_local_equiv.source) :
filter.map ⇑e (nhds_within x s) = nhds_within (⇑e x) t
@[protected]
theorem
local_homeomorph.is_image.closure
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
@[protected]
theorem
local_homeomorph.is_image.interior
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
@[protected]
theorem
local_homeomorph.is_image.frontier
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
theorem
local_homeomorph.is_image.is_open_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t) :
is_open (e.to_local_equiv.source ∩ s) ↔ is_open (e.to_local_equiv.target ∩ t)
def
local_homeomorph.is_image.restr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t)
(hs : is_open (e.to_local_equiv.source ∩ s)) :
local_homeomorph α β
Restrict a local_homeomorph to a pair of corresponding open sets.
Equations
- h.restr hs = {to_local_equiv := _.restr, open_source := hs, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
local_homeomorph.is_image.restr_to_local_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e : local_homeomorph α β}
{s : set α}
{t : set β}
(h : e.is_image s t)
(hs : is_open (e.to_local_equiv.source ∩ s)) :
(h.restr hs).to_local_equiv = _.restr
theorem
local_homeomorph.is_image_source_target
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
theorem
local_homeomorph.is_image_source_target_of_disjoint
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e e' : local_homeomorph α β)
(hs : disjoint e.to_local_equiv.source e'.to_local_equiv.source)
(ht : disjoint e.to_local_equiv.target e'.to_local_equiv.target) :
e.is_image e'.to_local_equiv.source e'.to_local_equiv.target
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_closure
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set β) :
theorem
local_homeomorph.preimage_frontier
{α : 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 α}
(hs : is_open s) :
theorem
local_homeomorph.image_open_of_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{s : set α}
(hs : is_open s)
(h : s ⊆ e.to_local_equiv.source) :
The image of an open set in the source is open.
theorem
local_homeomorph.image_open_of_open'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{s : set α}
(hs : is_open s) :
The image of the restriction of an open set to the source is open.
def
local_homeomorph.of_continuous_open_restrict
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_equiv α β)
(hc : continuous_on ⇑e e.source)
(ho : is_open_map (e.source.restrict ⇑e))
(hs : is_open e.source) :
local_homeomorph α β
A local_equiv with continuous open forward map and an open source is a local_homeomorph.
Equations
- local_homeomorph.of_continuous_open_restrict e hc ho hs = {to_local_equiv := e, open_source := hs, open_target := _, continuous_to_fun := hc, continuous_inv_fun := _}
def
local_homeomorph.of_continuous_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_equiv α β)
(hc : continuous_on ⇑e e.source)
(ho : is_open_map ⇑e)
(hs : is_open e.source) :
local_homeomorph α β
A local_equiv with continuous open forward map and an open source is a local_homeomorph.
Equations
- local_homeomorph.of_continuous_open e hc ho hs = local_homeomorph.of_continuous_open_restrict e hc _ hs
@[protected]
def
local_homeomorph.restr_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α)
(hs : is_open s) :
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 = _.restr _
@[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
theorem
local_homeomorph.restr_target
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α) :
@[protected]
def
local_homeomorph.restr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : 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
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
@[simp]
theorem
local_homeomorph.restr_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α) :
@[simp]
theorem
local_homeomorph.restr_symm_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α) :
@[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)
theorem
local_homeomorph.restr_source'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(s : set α)
(hs : 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 α)
(hs : 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 α}
(h : e.to_local_equiv.source ⊆ s) :
@[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 α) :
@[simp]
@[protected]
The identity on the whole space as a local homeomorphism.
Equations
@[simp]
@[simp]
def
local_homeomorph.of_set
{α : Type u_1}
[topological_space α]
(s : set α)
(hs : 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_apply
{α : Type u_1}
[topological_space α]
(s : set α)
(hs : is_open s) :
⇑(local_homeomorph.of_set s hs) = (local_equiv.of_set s).to_fun
theorem
local_homeomorph.of_set_source
{α : Type u_1}
[topological_space α]
(s : set α)
(hs : is_open s) :
theorem
local_homeomorph.of_set_target
{α : Type u_1}
[topological_space α]
(s : set α)
(hs : is_open s) :
@[simp]
theorem
local_homeomorph.of_set_to_local_equiv
{α : 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) :
(local_homeomorph.of_set s hs).symm = local_homeomorph.of_set s hs
@[simp]
@[protected]
def
local_homeomorph.trans'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : local_homeomorph β γ)
(h : 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 := _}
@[protected]
def
local_homeomorph.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : local_homeomorph β γ) :
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_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : local_homeomorph β γ)
{x : α} :
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.trans_homeomorph
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : β ≃ₜ γ) :
local_homeomorph α γ
Postcompose a local homeomorphism with an homeomorphism. We modify the source and target to have better definitional behavior.
Equations
- e.trans_homeomorph e' = {to_local_equiv := e.to_local_equiv.trans_equiv e'.to_equiv, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
local_homeomorph.trans_homeomorph_target
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : β ≃ₜ γ) :
(e.trans_homeomorph e').to_local_equiv.target = ⇑(e'.symm) ⁻¹' e.to_local_equiv.target
@[simp]
theorem
local_homeomorph.trans_homeomorph_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : β ≃ₜ γ) :
@[simp]
theorem
local_homeomorph.trans_homeomorph_symm_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : β ≃ₜ γ) :
@[simp]
theorem
local_homeomorph.trans_homeomorph_source
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : β ≃ₜ γ) :
theorem
local_homeomorph.trans_equiv_eq_trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
(e' : β ≃ₜ γ) :
e.trans_homeomorph e' = e.trans e'.to_local_homeomorph
@[simp]
theorem
homeomorph.trans_local_homeomorph_target
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e' : local_homeomorph β γ)
(e : α ≃ₜ β) :
def
homeomorph.trans_local_homeomorph
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e' : local_homeomorph β γ)
(e : α ≃ₜ β) :
local_homeomorph α γ
Precompose a local homeomorphism with an homeomorphism. We modify the source and target to have better definitional behavior.
Equations
- homeomorph.trans_local_homeomorph e' e = {to_local_equiv := equiv.trans_local_equiv e'.to_local_equiv e.to_equiv, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.trans_local_homeomorph_source
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e' : local_homeomorph β γ)
(e : α ≃ₜ β) :
@[simp]
theorem
homeomorph.trans_local_homeomorph_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e' : local_homeomorph β γ)
(e : α ≃ₜ β) :
@[simp]
theorem
homeomorph.trans_local_homeomorph_symm_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e' : local_homeomorph β γ)
(e : α ≃ₜ β) :
theorem
homeomorph.trans_local_homeomorph_eq_trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e' : local_homeomorph β γ)
(e : α ≃ₜ β) :
def
local_homeomorph.eq_on_source
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e e' : local_homeomorph α β) :
Prop
eq_on_source e e' means that e and e' have the same source, and coincide there. They
should really be considered the same local equiv.
Equations
- 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
@[protected, 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 α β}
(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}
[topological_space α]
[topological_space β]
{e e' : local_homeomorph α β}
(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}
[topological_space α]
[topological_space β]
{e e' : local_homeomorph α β}
(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}
[topological_space α]
[topological_space β]
{e e' : local_homeomorph α β}
(h : e ≈ e') :
set.eq_on ⇑e ⇑e' e.to_local_equiv.source
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 α β}
(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}
[topological_space α]
[topological_space β]
[topological_space γ]
{e e' : local_homeomorph α β}
{f f' : local_homeomorph β γ}
(he : e ≈ e')
(hf : f ≈ 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 α) :
Restriction of local homeomorphisms respects equivalence
theorem
local_homeomorph.set.eq_on.restr_eq_on_source
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{e e' : local_homeomorph α β}
(h : set.eq_on ⇑e ⇑e' (e.to_local_equiv.source ∩ e'.to_local_equiv.source)) :
e.restr e'.to_local_equiv.source ≈ e'.restr e.to_local_equiv.source
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 α β}
(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}
[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_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 ×ˢ e'.to_local_equiv.target
@[simp]
theorem
local_homeomorph.prod_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
(e : local_homeomorph α β)
(e' : local_homeomorph γ δ) :
def
local_homeomorph.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
(e : local_homeomorph α β)
(e' : local_homeomorph γ δ) :
local_homeomorph (α × γ) (β × δ)
The product of two local homeomorphisms, as a local homeomorphism on the product space.
Equations
- e.prod e' = {to_local_equiv := e.to_local_equiv.prod e'.to_local_equiv, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
theorem
local_homeomorph.prod_symm_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
(e : local_homeomorph α β)
(e' : local_homeomorph γ δ)
(p : β × δ) :
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 ×ˢ e'.to_local_equiv.source
@[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.refl_prod_refl
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
(local_homeomorph.refl α).prod (local_homeomorph.refl β) = local_homeomorph.refl (α × β)
@[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.prod_eq_prod_of_nonempty
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{e₁ e₁' : local_homeomorph α β}
{e₂ e₂' : local_homeomorph γ δ}
(h : (e₁.prod e₂).to_local_equiv.source.nonempty) :
theorem
local_homeomorph.prod_eq_prod_of_nonempty'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{e₁ e₁' : local_homeomorph α β}
{e₂ e₂' : local_homeomorph γ δ}
(h : (e₁'.prod e₂').to_local_equiv.source.nonempty) :
@[simp]
theorem
local_homeomorph.piecewise_to_local_equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e e' : local_homeomorph α β)
(s : set α)
(t : set β)
[Π (x : α), decidable (x ∈ s)]
[Π (y : β), decidable (y ∈ t)]
(H : e.is_image s t)
(H' : e'.is_image s t)
(Hs : e.to_local_equiv.source ∩ frontier s = e'.to_local_equiv.source ∩ frontier s)
(Heq : set.eq_on ⇑e ⇑e' (e.to_local_equiv.source ∩ frontier s)) :
(e.piecewise e' s t H H' Hs Heq).to_local_equiv = e.to_local_equiv.piecewise e'.to_local_equiv s t H H'
def
local_homeomorph.piecewise
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e e' : local_homeomorph α β)
(s : set α)
(t : set β)
[Π (x : α), decidable (x ∈ s)]
[Π (y : β), decidable (y ∈ t)]
(H : e.is_image s t)
(H' : e'.is_image s t)
(Hs : e.to_local_equiv.source ∩ frontier s = e'.to_local_equiv.source ∩ frontier s)
(Heq : set.eq_on ⇑e ⇑e' (e.to_local_equiv.source ∩ frontier s)) :
local_homeomorph α β
Combine two local_homeomorphs using set.piecewise. The source of the new local_homeomorph
is s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s, and similarly for target. The
function sends e.source ∩ s to e.target ∩ t using e and e'.source \ s to e'.target \ t
using e', and similarly for the inverse function. To ensure that the maps to_fun and inv_fun
are inverse of each other on the new source and target, the definition assumes that the sets s
and t are related both by e.is_image and e'.is_image. To ensure that the new maps are
continuous on source/target, it also assumes that e.source and e'.source meet frontier s
on the same set and e x = e' x on this intersection.
Equations
- e.piecewise e' s t H H' Hs Heq = {to_local_equiv := e.to_local_equiv.piecewise e'.to_local_equiv s t H H', open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
local_homeomorph.piecewise_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e e' : local_homeomorph α β)
(s : set α)
(t : set β)
[Π (x : α), decidable (x ∈ s)]
[Π (y : β), decidable (y ∈ t)]
(H : e.is_image s t)
(H' : e'.is_image s t)
(Hs : e.to_local_equiv.source ∩ frontier s = e'.to_local_equiv.source ∩ frontier s)
(Heq : set.eq_on ⇑e ⇑e' (e.to_local_equiv.source ∩ frontier s)) :
@[simp]
theorem
local_homeomorph.symm_piecewise
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e e' : local_homeomorph α β)
{s : set α}
{t : set β}
[Π (x : α), decidable (x ∈ s)]
[Π (y : β), decidable (y ∈ t)]
(H : e.is_image s t)
(H' : e'.is_image s t)
(Hs : e.to_local_equiv.source ∩ frontier s = e'.to_local_equiv.source ∩ frontier s)
(Heq : set.eq_on ⇑e ⇑e' (e.to_local_equiv.source ∩ frontier s)) :
def
local_homeomorph.disjoint_union
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e e' : local_homeomorph α β)
[Π (x : α), decidable (x ∈ e.to_local_equiv.source)]
[Π (y : β), decidable (y ∈ e.to_local_equiv.target)]
(Hs : disjoint e.to_local_equiv.source e'.to_local_equiv.source)
(Ht : disjoint e.to_local_equiv.target e'.to_local_equiv.target) :
local_homeomorph α β
Combine two local_homeomorphs with disjoint sources and disjoint targets. We reuse
local_homeomorph.piecewise then override to_local_equiv to local_equiv.disjoint_union.
This way we have better definitional equalities for source and target.
Equations
- e.disjoint_union e' Hs Ht = (e.piecewise e' e.to_local_equiv.source e.to_local_equiv.target _ _ _ _).replace_equiv (e.to_local_equiv.disjoint_union e'.to_local_equiv Hs Ht) _
def
local_homeomorph.pi
{ι : Type u_5}
[fintype ι]
{Xi : ι → Type u_6}
{Yi : ι → Type u_7}
[Π (i : ι), topological_space (Xi i)]
[Π (i : ι), topological_space (Yi i)]
(ei : Π (i : ι), local_homeomorph (Xi i) (Yi i)) :
local_homeomorph (Π (i : ι), Xi i) (Π (i : ι), Yi i)
The product of a finite family of local_homeomorphs.
Equations
- local_homeomorph.pi ei = {to_local_equiv := local_equiv.pi (λ (i : ι), (ei i).to_local_equiv), open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
@[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_homeomorph.pi ei).to_local_equiv = 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}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
{f : β → γ}
{s : set β}
{x : β}
(h : 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 : β}
(h : 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 β}
(h : 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 : γ}
(hx : f x ∈ e.to_local_equiv.source)
(h : 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 : γ}
(h : 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 γ}
(h : 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.
theorem
local_homeomorph.continuous_iff_continuous_comp_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(e : local_homeomorph α β)
{f : γ → α}
(h : f ⁻¹' e.to_local_equiv.source = set.univ) :
continuous f ↔ continuous (⇑e ∘ f)
A function is continuous if and only if its composition with a local homeomorphism on the left is continuous and its image is contained in the source.
def
local_homeomorph.homeomorph_of_image_subset_source
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{s : set α}
{t : set β}
(hs : s ⊆ e.to_local_equiv.source)
(ht : ⇑e '' s = t) :
The homeomorphism obtained by restricting a local_homeomorph to a subset of the source.
@[simp]
theorem
local_homeomorph.homeomorph_of_image_subset_source_apply_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{s : set α}
{t : set β}
(hs : s ⊆ e.to_local_equiv.source)
(ht : ⇑e '' s = t)
(a : ↥s) :
@[simp]
theorem
local_homeomorph.homeomorph_of_image_subset_source_symm_apply_coe
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{s : set α}
{t : set β}
(hs : s ⊆ e.to_local_equiv.source)
(ht : ⇑e '' s = t)
(b : ↥t) :
def
local_homeomorph.to_homeomorph_source_target
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β) :
↥(e.to_local_equiv.source) ≃ₜ ↥(e.to_local_equiv.target)
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}
[topological_space α]
[topological_space β]
[topological_space.second_countable_topology β]
(e : local_homeomorph α β) :
@[simp]
theorem
local_homeomorph.to_homeomorph_of_source_eq_univ_target_eq_univ_symm_apply
{α : 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_of_source_eq_univ_target_eq_univ_apply
{α : 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) :
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 α β)
(h : e.to_local_equiv.source = set.univ)
(h' : 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 := _}
theorem
local_homeomorph.to_open_embedding
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
(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]
@[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
noncomputable
def
open_embedding.to_local_homeomorph
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α → β)
(h : open_embedding f)
[nonempty α] :
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
@[simp]
theorem
open_embedding.to_local_homeomorph_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α → β)
(h : open_embedding f)
[nonempty α] :
⇑(open_embedding.to_local_homeomorph f h) = f
@[simp]
theorem
open_embedding.to_local_homeomorph_source
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α → β)
(h : open_embedding f)
[nonempty α] :
@[simp]
theorem
open_embedding.to_local_homeomorph_target
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α → β)
(h : open_embedding f)
[nonempty α] :
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)
noncomputable
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] :
noncomputable
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] :
@[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.map_subtype_source
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{s : topological_space.opens α}
[nonempty ↥s]
{x : ↥s}
(hxe : ↑x ∈ e.to_local_equiv.source) :
⇑e ↑x ∈ (e.subtype_restr s).to_local_equiv.target
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)
theorem
local_homeomorph.subtype_restr_symm_eq_on_of_le
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(e : local_homeomorph α β)
{U V : topological_space.opens α}
[nonempty ↥U]
[nonempty ↥V]
(hUV : U ≤ V) :
set.eq_on ⇑((e.subtype_restr V).symm) (set.inclusion hUV ∘ ⇑((e.subtype_restr U).symm)) (e.subtype_restr U).to_local_equiv.target