Local homeomorphisms

This file defines homeomorphisms between open subsets of topological spaces. An element e of LocalHomeomorph α β is an extension of LocalEquiv α β, i.e., it is a pair of functions e.toFun and e.invFun, 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.toFun x and e.invFun x.

Main definitions

Homeomorph.toLocalHomeomorph : associating a local homeomorphism to a homeomorphism, with source = target = Set.univ; LocalHomeomorph.symm : the inverse of a local homeomorphism LocalHomeomorph.trans : the composition of two local homeomorphisms LocalHomeomorph.refl : the identity local homeomorphism LocalHomeomorph.ofSet : the identity on a set s LocalHomeomorph.EqOnSource : equivalence relation describing the "right" notion of equality for local homeomorphisms

Implementation notes

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

For design notes, see LocalEquiv.lean.

Local coding conventions

If a lemma deals with the intersection of a set with either source or target of a LocalEquiv, then it should use e.source ∩ s or e.target ∩ t, not s ∩ e.source or t ∩ e.target.

structure LocalHomeomorph (α : Type u_5) (β : Type u_6) [TopologicalSpace α] [TopologicalSpace β] extends LocalEquiv : Type (max u_5 u_6)

• toFun : α → β
• invFun : β → α
• source : Set α
• target : Set β
• map_source' : ∀ ⦃x : α⦄, x ∈ s.source → ↑s.toLocalEquiv x ∈ s.target
• map_target' : ∀ ⦃x : β⦄, x ∈ s.target → LocalEquiv.invFun s.toLocalEquiv x ∈ s.source
• left_inv' : ∀ ⦃x : α⦄, x ∈ s.source → LocalEquiv.invFun s.toLocalEquiv (↑s.toLocalEquiv x) = x
• right_inv' : ∀ ⦃x : β⦄, x ∈ s.target → ↑s.toLocalEquiv (LocalEquiv.invFun s.toLocalEquiv x) = x
• open_source : IsOpen s.source
• open_target : IsOpen s.target
• continuous_toFun : ContinuousOn (↑s.toLocalEquiv) s.source
• continuous_invFun : ContinuousOn s.invFun s.target

local homeomorphisms, defined on open subsets of the space

def LocalHomeomorph.toFun' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : α → β

Coercion of a local homeomorphisms to a function. We don't use e.toFun because it is actually e.toLocalEquiv.toFun, so simp will apply lemmas about toLocalEquiv. While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs.

Equations

• ↑e = ↑e.toLocalEquiv

instance LocalHomeomorph.instCoeFunLocalHomeomorphForAll {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : CoeFun (LocalHomeomorph α β) fun x => α → β

Coercion of a LocalHomeomorph to function. Note that a LocalHomeomorph is not FunLike.

Equations

• LocalHomeomorph.instCoeFunLocalHomeomorphForAll = { coe := fun e => ↑e }

def LocalHomeomorph.symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : LocalHomeomorph β α

The inverse of a local homeomorphism

Equations

• One or more equations did not get rendered due to their size.

def LocalHomeomorph.Simps.apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : α → β

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

Equations

• LocalHomeomorph.Simps.apply e = ↑e

def LocalHomeomorph.Simps.symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : β → α

See Note [custom simps projection]

Equations

• LocalHomeomorph.Simps.symm_apply e = ↑(LocalHomeomorph.symm e)

theorem LocalHomeomorph.continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : ContinuousOn (↑e) e.source

theorem LocalHomeomorph.continuousOn_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : ContinuousOn (↑(LocalHomeomorph.symm e)) e.target

@[simp]

theorem LocalHomeomorph.mk_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalEquiv α β) (a : IsOpen e.source) (b : IsOpen e.target) (c : ContinuousOn (↑e) e.source) (d : ContinuousOn e.invFun e.target) : ↑{ toLocalEquiv := e, open_source := a, open_target := b, continuous_toFun := c, continuous_invFun := d } = ↑e

@[simp]

theorem LocalHomeomorph.mk_coe_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalEquiv α β) (a : IsOpen e.source) (b : IsOpen e.target) (c : ContinuousOn (↑e) e.source) (d : ContinuousOn e.invFun e.target) : ↑(LocalHomeomorph.symm { toLocalEquiv := e, open_source := a, open_target := b, continuous_toFun := c, continuous_invFun := d }) = ↑(LocalEquiv.symm e)

theorem LocalHomeomorph.toLocalEquiv_injective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : Function.Injective LocalHomeomorph.toLocalEquiv

@[simp]

theorem LocalHomeomorph.toFun_eq_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : ↑e.toLocalEquiv = ↑e

@[simp]

theorem LocalHomeomorph.invFun_eq_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : e.invFun = ↑(LocalHomeomorph.symm e)

@[simp]

theorem LocalHomeomorph.coe_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : ↑e.toLocalEquiv = ↑e

@[simp]

theorem LocalHomeomorph.coe_coe_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : ↑(LocalEquiv.symm e.toLocalEquiv) = ↑(LocalHomeomorph.symm e)

@[simp]

theorem LocalHomeomorph.map_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (h : x ∈ e.source) : ↑e x ∈ e.target

@[simp]

theorem LocalHomeomorph.map_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : β} (h : x ∈ e.target) : ↑(LocalHomeomorph.symm e) x ∈ e.source

@[simp]

theorem LocalHomeomorph.left_inv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (h : x ∈ e.source) : ↑(LocalHomeomorph.symm e) (↑e x) = x

@[simp]

theorem LocalHomeomorph.right_inv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : β} (h : x ∈ e.target) : ↑e (↑(LocalHomeomorph.symm e) x) = x

theorem LocalHomeomorph.eq_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.target) : x = ↑(LocalHomeomorph.symm e) y ↔ ↑e x = y

theorem LocalHomeomorph.mapsTo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : Set.MapsTo (↑e) e.source e.target

theorem LocalHomeomorph.symm_mapsTo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : Set.MapsTo (↑(LocalHomeomorph.symm e)) e.target e.source

theorem LocalHomeomorph.leftInvOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : Set.LeftInvOn (↑(LocalHomeomorph.symm e)) (↑e) e.source

theorem LocalHomeomorph.rightInvOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : Set.RightInvOn (↑(LocalHomeomorph.symm e)) (↑e) e.target

theorem LocalHomeomorph.invOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : Set.InvOn (↑(LocalHomeomorph.symm e)) (↑e) e.source e.target

theorem LocalHomeomorph.injOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : Set.InjOn (↑e) e.source

theorem LocalHomeomorph.bijOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : Set.BijOn (↑e) e.source e.target

theorem LocalHomeomorph.surjOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : Set.SurjOn (↑e) e.source e.target

@[simp]

theorem Homeomorph.toLocalHomeomorphOfImageEq_toLocalEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (s : Set α) (hs : IsOpen s) (t : Set β) (h : ↑e '' s = t) : (Homeomorph.toLocalHomeomorphOfImageEq e s hs t h).toLocalEquiv = Equiv.toLocalEquivOfImageEq e.toEquiv s t h

@[simp]

theorem Homeomorph.toLocalHomeomorphOfImageEq_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (s : Set α) (hs : IsOpen s) (t : Set β) (h : ↑e '' s = t) : ↑(LocalHomeomorph.symm (Homeomorph.toLocalHomeomorphOfImageEq e s hs t h)) = ↑(Homeomorph.symm e)

@[simp]

theorem Homeomorph.toLocalHomeomorphOfImageEq_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (s : Set α) (hs : IsOpen s) (t : Set β) (h : ↑e '' s = t) : ↑(Homeomorph.toLocalHomeomorphOfImageEq e s hs t h) = ↑e

theorem Homeomorph.toLocalHomeomorphOfImageEq_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (s : Set α) (hs : IsOpen s) (t : Set β) (h : ↑e '' s = t) : (Homeomorph.toLocalHomeomorphOfImageEq e s hs t h).toLocalEquiv.source = s

theorem Homeomorph.toLocalHomeomorphOfImageEq_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (s : Set α) (hs : IsOpen s) (t : Set β) (h : ↑e '' s = t) : (Homeomorph.toLocalHomeomorphOfImageEq e s hs t h).toLocalEquiv.target = t

def Homeomorph.toLocalHomeomorphOfImageEq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) (s : Set α) (hs : IsOpen s) (t : Set β) (h : ↑e '' s = t) : LocalHomeomorph α β

Interpret a Homeomorph as a LocalHomeomorph by restricting it to an open set s in the domain and to t in the codomain.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Homeomorph.toLocalHomeomorph_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) : ↑(LocalHomeomorph.symm (Homeomorph.toLocalHomeomorph e)) = ↑(Homeomorph.symm e)

@[simp]

theorem Homeomorph.toLocalHomeomorph_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) : ↑(Homeomorph.toLocalHomeomorph e) = ↑e

@[simp]

theorem Homeomorph.toLocalHomeomorph_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) : (Homeomorph.toLocalHomeomorph e).toLocalEquiv.source = Set.univ

@[simp]

theorem Homeomorph.toLocalHomeomorph_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) : (Homeomorph.toLocalHomeomorph e).toLocalEquiv.target = Set.univ

def Homeomorph.toLocalHomeomorph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) : LocalHomeomorph α β

A homeomorphism induces a local homeomorphism on the whole space

Equations

• Homeomorph.toLocalHomeomorph e = Homeomorph.toLocalHomeomorphOfImageEq e Set.univ (_ : IsOpen Set.univ) Set.univ (_ : ↑e '' Set.univ = Set.univ)

def LocalHomeomorph.replaceEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalEquiv α β) (h : e.toLocalEquiv = e') : LocalHomeomorph α β

Replace toLocalEquiv field to provide better definitional equalities.

Equations

• One or more equations did not get rendered due to their size.

theorem LocalHomeomorph.replaceEquiv_eq_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalEquiv α β) (h : e.toLocalEquiv = e') : LocalHomeomorph.replaceEquiv e e' h = e

theorem LocalHomeomorph.source_preimage_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : e.source ⊆ ↑e ⁻¹' e.target

@[deprecated LocalHomeomorph.toLocalEquiv_injective]

theorem LocalHomeomorph.eq_of_localEquiv_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} (h : e.toLocalEquiv = e'.toLocalEquiv) : e = e'

theorem LocalHomeomorph.eventually_left_inverse {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) : ∀ᶠ (y : α) in nhds x, ↑(LocalHomeomorph.symm e) (↑e y) = y

theorem LocalHomeomorph.eventually_left_inverse' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : β} (hx : x ∈ e.target) : ∀ᶠ (y : α) in nhds (↑(LocalHomeomorph.symm e) x), ↑(LocalHomeomorph.symm e) (↑e y) = y

theorem LocalHomeomorph.eventually_right_inverse {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : β} (hx : x ∈ e.target) : ∀ᶠ (y : β) in nhds x, ↑e (↑(LocalHomeomorph.symm e) y) = y

theorem LocalHomeomorph.eventually_right_inverse' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) : ∀ᶠ (y : β) in nhds (↑e x), ↑e (↑(LocalHomeomorph.symm e) y) = y

theorem LocalHomeomorph.eventually_ne_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) : ∀ᶠ (x' : α) in nhdsWithin x {x}ᶜ, ↑e x' ≠ ↑e x

theorem LocalHomeomorph.nhdsWithin_source_inter {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) (s : Set α) : nhdsWithin x (e.source ∩ s) = nhdsWithin x s

theorem LocalHomeomorph.nhdsWithin_target_inter {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : β} (hx : x ∈ e.target) (s : Set β) : nhdsWithin x (e.target ∩ s) = nhdsWithin x s

theorem LocalHomeomorph.image_eq_target_inter_inv_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set α} (h : s ⊆ e.source) : ↑e '' s = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s

theorem LocalHomeomorph.image_source_inter_eq' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) : ↑e '' (e.source ∩ s) = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s

theorem LocalHomeomorph.image_source_inter_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) : ↑e '' (e.source ∩ s) = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (e.source ∩ s)

theorem LocalHomeomorph.symm_image_eq_source_inter_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set β} (h : s ⊆ e.target) : ↑(LocalHomeomorph.symm e) '' s = e.source ∩ ↑e ⁻¹' s

theorem LocalHomeomorph.symm_image_target_inter_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set β) : ↑(LocalHomeomorph.symm e) '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' (e.target ∩ s)

theorem LocalHomeomorph.source_inter_preimage_inv_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) : e.source ∩ ↑e ⁻¹' (↑(LocalHomeomorph.symm e) ⁻¹' s) = e.source ∩ s

theorem LocalHomeomorph.target_inter_inv_preimage_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set β) : e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (↑e ⁻¹' s) = e.target ∩ s

theorem LocalHomeomorph.source_inter_preimage_target_inter {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set β) : e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s

theorem LocalHomeomorph.image_source_eq_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : ↑e '' e.source = e.target

theorem LocalHomeomorph.symm_image_target_eq_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : ↑(LocalHomeomorph.symm e) '' e.target = e.source

theorem LocalHomeomorph.ext {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalHomeomorph α β) (h : ∀ (x : α), ↑e x = ↑e' x) (hinv : ∀ (x : β), ↑(LocalHomeomorph.symm e) x = ↑(LocalHomeomorph.symm e') x) (hs : e.source = e'.source) : e = e'

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

theorem LocalHomeomorph.ext_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} : e = e' ↔ (∀ (x : α), ↑e x = ↑e' x) ∧ (∀ (x : β), ↑(LocalHomeomorph.symm e) x = ↑(LocalHomeomorph.symm e') x) ∧ e.source = e'.source

@[simp]

theorem LocalHomeomorph.symm_toLocalEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : (LocalHomeomorph.symm e).toLocalEquiv = LocalEquiv.symm e.toLocalEquiv

theorem LocalHomeomorph.symm_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : (LocalHomeomorph.symm e).toLocalEquiv.source = e.target

theorem LocalHomeomorph.symm_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : (LocalHomeomorph.symm e).toLocalEquiv.target = e.source

@[simp]

theorem LocalHomeomorph.symm_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : LocalHomeomorph.symm (LocalHomeomorph.symm e) = e

theorem LocalHomeomorph.continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (h : x ∈ e.source) : ContinuousAt (↑e) x

A local homeomorphism is continuous at any point of its source

theorem LocalHomeomorph.continuousAt_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : β} (h : x ∈ e.target) : ContinuousAt (↑(LocalHomeomorph.symm e)) x

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

theorem LocalHomeomorph.tendsto_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) : Filter.Tendsto (↑(LocalHomeomorph.symm e)) (nhds (↑e x)) (nhds x)

theorem LocalHomeomorph.map_nhds_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) : Filter.map (↑e) (nhds x) = nhds (↑e x)

theorem LocalHomeomorph.symm_map_nhds_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) : Filter.map (↑(LocalHomeomorph.symm e)) (nhds (↑e x)) = nhds x

theorem LocalHomeomorph.image_mem_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) {s : Set α} (hs : s ∈ nhds x) : ↑e '' s ∈ nhds (↑e x)

theorem LocalHomeomorph.map_nhdsWithin_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) (s : Set α) : Filter.map (↑e) (nhdsWithin x s) = nhdsWithin (↑e x) (↑e '' (e.source ∩ s))

theorem LocalHomeomorph.map_nhdsWithin_preimage_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) (s : Set β) : Filter.map (↑e) (nhdsWithin x (↑e ⁻¹' s)) = nhdsWithin (↑e x) s

theorem LocalHomeomorph.eventually_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (p : β → Prop) (hx : x ∈ e.source) : (∀ᶠ (y : β) in nhds (↑e x), p y) ↔ ∀ᶠ (x : α) in nhds x, p (↑e x)

theorem LocalHomeomorph.eventually_nhds' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (p : α → Prop) (hx : x ∈ e.source) : (∀ᶠ (y : β) in nhds (↑e x), p (↑(LocalHomeomorph.symm e) y)) ↔ ∀ᶠ (x : α) in nhds x, p x

theorem LocalHomeomorph.eventually_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (p : β → Prop) {s : Set α} (hx : x ∈ e.source) : (∀ᶠ (y : β) in nhdsWithin (↑e x) (↑(LocalHomeomorph.symm e) ⁻¹' s), p y) ↔ ∀ᶠ (x : α) in nhdsWithin x s, p (↑e x)

theorem LocalHomeomorph.eventually_nhdsWithin' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (p : α → Prop) {s : Set α} (hx : x ∈ e.source) : (∀ᶠ (y : β) in nhdsWithin (↑e x) (↑(LocalHomeomorph.symm e) ⁻¹' s), p (↑(LocalHomeomorph.symm e) y)) ↔ ∀ᶠ (x : α) in nhdsWithin x s, p x

theorem LocalHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {e : LocalHomeomorph α β} {s : Set α} {t : Set γ} {x : α} {f : α → γ} (hf : ContinuousWithinAt f s x) (hxe : x ∈ e.source) (ht : t ∈ nhds (f x)) : ↑(LocalHomeomorph.symm e) ⁻¹' s =ᶠ[nhds (↑e x)] e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (s ∩ f ⁻¹' t)

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 LocalHomeomorph.preimage_open_of_open {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set β} (hs : IsOpen s) : IsOpen (e.source ∩ ↑e ⁻¹' s)

LocalHomeomorph.IsImage 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 LocalEquiv.IsImage for local homeomorphisms. In this section we transfer API about LocalEquiv.IsImage to local homeomorphisms and add a few LocalHomeomorph-specific lemmas like LocalHomeomorph.IsImage.closure.

def LocalHomeomorph.IsImage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) (t : Set β) : Prop

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

• e '' (e.source ∩ s) = e.target ∩ t;
• e.source ∩ e ⁻¹ t = e.source ∩ s;
• ∀ x ∈ e.source, e x ∈ t ↔ x ∈ s (this one is used in the definition).

Equations

• LocalHomeomorph.IsImage e s t = ∀ ⦃x : α⦄, x ∈ e.source → (↑e x ∈ t ↔ x ∈ s)

theorem LocalHomeomorph.IsImage.toLocalEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : LocalEquiv.IsImage e.toLocalEquiv s t

theorem LocalHomeomorph.IsImage.apply_mem_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} {x : α} (h : LocalHomeomorph.IsImage e s t) (hx : x ∈ e.source) : ↑e x ∈ t ↔ x ∈ s

theorem LocalHomeomorph.IsImage.symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : LocalHomeomorph.IsImage (LocalHomeomorph.symm e) t s

theorem LocalHomeomorph.IsImage.symm_apply_mem_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} {y : β} (h : LocalHomeomorph.IsImage e s t) (hy : y ∈ e.target) : ↑(LocalHomeomorph.symm e) y ∈ s ↔ y ∈ t

@[simp]

theorem LocalHomeomorph.IsImage.symm_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : LocalHomeomorph.IsImage (LocalHomeomorph.symm e) t s ↔ LocalHomeomorph.IsImage e s t

theorem LocalHomeomorph.IsImage.mapsTo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : Set.MapsTo (↑e) (e.source ∩ s) (e.target ∩ t)

theorem LocalHomeomorph.IsImage.symm_mapsTo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : Set.MapsTo (↑(LocalHomeomorph.symm e)) (e.target ∩ t) (e.source ∩ s)

theorem LocalHomeomorph.IsImage.image_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : ↑e '' (e.source ∩ s) = e.target ∩ t

theorem LocalHomeomorph.IsImage.symm_image_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : ↑(LocalHomeomorph.symm e) '' (e.target ∩ t) = e.source ∩ s

theorem LocalHomeomorph.IsImage.iff_preimage_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : LocalHomeomorph.IsImage e s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s

theorem LocalHomeomorph.IsImage.of_preimage_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : e.source ∩ ↑e ⁻¹' t = e.source ∩ s → LocalHomeomorph.IsImage e s t

Alias of the reverse direction of LocalHomeomorph.IsImage.iff_preimage_eq.

theorem LocalHomeomorph.IsImage.preimage_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : LocalHomeomorph.IsImage e s t → e.source ∩ ↑e ⁻¹' t = e.source ∩ s

Alias of the forward direction of LocalHomeomorph.IsImage.iff_preimage_eq.

theorem LocalHomeomorph.IsImage.iff_symm_preimage_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : LocalHomeomorph.IsImage e s t ↔ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s = e.target ∩ t

theorem LocalHomeomorph.IsImage.symm_preimage_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : LocalHomeomorph.IsImage e s t → e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s = e.target ∩ t

Alias of the forward direction of LocalHomeomorph.IsImage.iff_symm_preimage_eq.

theorem LocalHomeomorph.IsImage.of_symm_preimage_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s = e.target ∩ t → LocalHomeomorph.IsImage e s t

Alias of the reverse direction of LocalHomeomorph.IsImage.iff_symm_preimage_eq.

theorem LocalHomeomorph.IsImage.iff_symm_preimage_eq' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : LocalHomeomorph.IsImage e s t ↔ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (e.source ∩ s) = e.target ∩ t

theorem LocalHomeomorph.IsImage.of_symm_preimage_eq' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (e.source ∩ s) = e.target ∩ t → LocalHomeomorph.IsImage e s t

Alias of the reverse direction of LocalHomeomorph.IsImage.iff_symm_preimage_eq'.

theorem LocalHomeomorph.IsImage.symm_preimage_eq' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : LocalHomeomorph.IsImage e s t → e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (e.source ∩ s) = e.target ∩ t

Alias of the forward direction of LocalHomeomorph.IsImage.iff_symm_preimage_eq'.

theorem LocalHomeomorph.IsImage.iff_preimage_eq' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : LocalHomeomorph.IsImage e s t ↔ e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s

theorem LocalHomeomorph.IsImage.preimage_eq' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : LocalHomeomorph.IsImage e s t → e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s

Alias of the forward direction of LocalHomeomorph.IsImage.iff_preimage_eq'.

theorem LocalHomeomorph.IsImage.of_preimage_eq' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} : e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s → LocalHomeomorph.IsImage e s t

Alias of the reverse direction of LocalHomeomorph.IsImage.iff_preimage_eq'.

theorem LocalHomeomorph.IsImage.of_image_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : ↑e '' (e.source ∩ s) = e.target ∩ t) : LocalHomeomorph.IsImage e s t

theorem LocalHomeomorph.IsImage.of_symm_image_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : ↑(LocalHomeomorph.symm e) '' (e.target ∩ t) = e.source ∩ s) : LocalHomeomorph.IsImage e s t

theorem LocalHomeomorph.IsImage.compl {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : LocalHomeomorph.IsImage e sᶜ tᶜ

theorem LocalHomeomorph.IsImage.inter {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β} (h : LocalHomeomorph.IsImage e s t) (h' : LocalHomeomorph.IsImage e s' t') : LocalHomeomorph.IsImage e (s ∩ s') (t ∩ t')

theorem LocalHomeomorph.IsImage.union {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β} (h : LocalHomeomorph.IsImage e s t) (h' : LocalHomeomorph.IsImage e s' t') : LocalHomeomorph.IsImage e (s ∪ s') (t ∪ t')

theorem LocalHomeomorph.IsImage.diff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β} (h : LocalHomeomorph.IsImage e s t) (h' : LocalHomeomorph.IsImage e s' t') : LocalHomeomorph.IsImage e (s \ s') (t \ t')

theorem LocalHomeomorph.IsImage.leftInvOn_piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} {e' : LocalHomeomorph α β} [(i : α) → Decidable (i ∈ s)] [(i : β) → Decidable (i ∈ t)] (h : LocalHomeomorph.IsImage e s t) (h' : LocalHomeomorph.IsImage e' s t) : Set.LeftInvOn (Set.piecewise t ↑(LocalHomeomorph.symm e) ↑(LocalHomeomorph.symm e')) (Set.piecewise s ↑e ↑e') (Set.ite s e.source e'.source)

theorem LocalHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} {e' : LocalHomeomorph α β} (h : LocalHomeomorph.IsImage e s t) (h' : LocalHomeomorph.IsImage e' s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)) : e.target ∩ t = e'.target ∩ t

theorem LocalHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} {e' : LocalHomeomorph α β} (h : LocalHomeomorph.IsImage e s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)) : Set.EqOn (↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e')) (e.target ∩ t)

theorem LocalHomeomorph.IsImage.map_nhdsWithin_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} {x : α} (h : LocalHomeomorph.IsImage e s t) (hx : x ∈ e.source) : Filter.map (↑e) (nhdsWithin x s) = nhdsWithin (↑e x) t

theorem LocalHomeomorph.IsImage.closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : LocalHomeomorph.IsImage e (closure s) (closure t)

theorem LocalHomeomorph.IsImage.interior {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : LocalHomeomorph.IsImage e (interior s) (interior t)

theorem LocalHomeomorph.IsImage.frontier {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : LocalHomeomorph.IsImage e (frontier s) (frontier t)

theorem LocalHomeomorph.IsImage.isOpen_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) : IsOpen (e.source ∩ s) ↔ IsOpen (e.target ∩ t)

@[simp]

theorem LocalHomeomorph.IsImage.restr_toLocalEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) (hs : IsOpen (e.source ∩ s)) : (LocalHomeomorph.IsImage.restr h hs).toLocalEquiv = LocalEquiv.IsImage.restr (_ : LocalEquiv.IsImage e.toLocalEquiv s t)

def LocalHomeomorph.IsImage.restr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} {t : Set β} (h : LocalHomeomorph.IsImage e s t) (hs : IsOpen (e.source ∩ s)) : LocalHomeomorph α β

Restrict a LocalHomeomorph to a pair of corresponding open sets.

Equations

• One or more equations did not get rendered due to their size.

theorem LocalHomeomorph.isImage_source_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : LocalHomeomorph.IsImage e e.source e.target

theorem LocalHomeomorph.isImage_source_target_of_disjoint {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalHomeomorph α β) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) : LocalHomeomorph.IsImage e e'.source e'.target

theorem LocalHomeomorph.preimage_interior {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set β) : e.source ∩ ↑e ⁻¹' interior s = e.source ∩ interior (↑e ⁻¹' s)

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

theorem LocalHomeomorph.preimage_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set β) : e.source ∩ ↑e ⁻¹' closure s = e.source ∩ closure (↑e ⁻¹' s)

theorem LocalHomeomorph.preimage_frontier {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set β) : e.source ∩ ↑e ⁻¹' frontier s = e.source ∩ frontier (↑e ⁻¹' s)

theorem LocalHomeomorph.preimage_open_of_open_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set α} (hs : IsOpen s) : IsOpen (e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' s)

theorem LocalHomeomorph.image_open_of_open {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set α} (hs : IsOpen s) (h : s ⊆ e.source) : IsOpen (↑e '' s)

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

theorem LocalHomeomorph.image_open_of_open' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set α} (hs : IsOpen s) : IsOpen (↑e '' (e.source ∩ s))

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

def LocalHomeomorph.ofContinuousOpenRestrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalEquiv α β) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (Set.restrict e.source ↑e)) (hs : IsOpen e.source) : LocalHomeomorph α β

A LocalEquiv with continuous open forward map and an open source is a LocalHomeomorph.

Equations

• One or more equations did not get rendered due to their size.

def LocalHomeomorph.ofContinuousOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalEquiv α β) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source) : LocalHomeomorph α β

A LocalEquiv with continuous open forward map and an open source is a LocalHomeomorph.

Equations

• LocalHomeomorph.ofContinuousOpen e hc ho hs = LocalHomeomorph.ofContinuousOpenRestrict e hc (_ : IsOpenMap (Set.restrict e.source ↑e)) hs

def LocalHomeomorph.restrOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) (hs : IsOpen s) : LocalHomeomorph α β

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

• LocalHomeomorph.restrOpen e s hs = LocalHomeomorph.IsImage.restr (_ : LocalHomeomorph.IsImage e s (↑(LocalHomeomorph.symm e) ⁻¹' s)) (_ : IsOpen (e.source ∩ s))

@[simp]

theorem LocalHomeomorph.restrOpen_toLocalEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) (hs : IsOpen s) : (LocalHomeomorph.restrOpen e s hs).toLocalEquiv = LocalEquiv.restr e.toLocalEquiv s

theorem LocalHomeomorph.restrOpen_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) (hs : IsOpen s) : (LocalHomeomorph.restrOpen e s hs).toLocalEquiv.source = e.source ∩ s

@[simp]

theorem LocalHomeomorph.restr_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) : ↑(LocalHomeomorph.symm (LocalHomeomorph.restr e s)) = ↑(LocalHomeomorph.symm e)

@[simp]

theorem LocalHomeomorph.restr_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) : ↑(LocalHomeomorph.restr e s) = ↑e

theorem LocalHomeomorph.restr_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) : (LocalHomeomorph.restr e s).toLocalEquiv.source = e.source ∩ interior s

theorem LocalHomeomorph.restr_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) : (LocalHomeomorph.restr e s).toLocalEquiv.target = e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' interior s

def LocalHomeomorph.restr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) : LocalHomeomorph α β

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

• LocalHomeomorph.restr e s = LocalHomeomorph.restrOpen e (interior s) (_ : IsOpen (interior s))

@[simp]

theorem LocalHomeomorph.restr_toLocalEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) : (LocalHomeomorph.restr e s).toLocalEquiv = LocalEquiv.restr e.toLocalEquiv (interior s)

theorem LocalHomeomorph.restr_source' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) (hs : IsOpen s) : (LocalHomeomorph.restr e s).toLocalEquiv.source = e.source ∩ s

theorem LocalHomeomorph.restr_toLocalEquiv' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) (hs : IsOpen s) : (LocalHomeomorph.restr e s).toLocalEquiv = LocalEquiv.restr e.toLocalEquiv s

theorem LocalHomeomorph.restr_eq_of_source_subset {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {s : Set α} (h : e.source ⊆ s) : LocalHomeomorph.restr e s = e

@[simp]

theorem LocalHomeomorph.restr_univ {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} : LocalHomeomorph.restr e Set.univ = e

theorem LocalHomeomorph.restr_source_inter {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : Set α) : LocalHomeomorph.restr e (e.source ∩ s) = LocalHomeomorph.restr e s

@[simp]

theorem LocalHomeomorph.refl_apply (α : Type u_5) [TopologicalSpace α] : ↑(LocalHomeomorph.refl α) = id

theorem LocalHomeomorph.refl_source (α : Type u_5) [TopologicalSpace α] : (LocalHomeomorph.refl α).toLocalEquiv.source = Set.univ

theorem LocalHomeomorph.refl_target (α : Type u_5) [TopologicalSpace α] : (LocalHomeomorph.refl α).toLocalEquiv.target = Set.univ

def LocalHomeomorph.refl (α : Type u_5) [TopologicalSpace α] : LocalHomeomorph α α

The identity on the whole space as a local homeomorphism.

Equations

• LocalHomeomorph.refl α = Homeomorph.toLocalHomeomorph (Homeomorph.refl α)

@[simp]

theorem LocalHomeomorph.refl_localEquiv {α : Type u_1} [TopologicalSpace α] : (LocalHomeomorph.refl α).toLocalEquiv = LocalEquiv.refl α

@[simp]

theorem LocalHomeomorph.refl_symm {α : Type u_1} [TopologicalSpace α] : LocalHomeomorph.symm (LocalHomeomorph.refl α) = LocalHomeomorph.refl α

@[simp]

theorem LocalHomeomorph.ofSet_apply {α : Type u_1} [TopologicalSpace α] (s : Set α) (hs : IsOpen s) : ↑(LocalHomeomorph.ofSet s hs) = id

theorem LocalHomeomorph.ofSet_source {α : Type u_1} [TopologicalSpace α] (s : Set α) (hs : IsOpen s) : (LocalHomeomorph.ofSet s hs).toLocalEquiv.source = s

theorem LocalHomeomorph.ofSet_target {α : Type u_1} [TopologicalSpace α] (s : Set α) (hs : IsOpen s) : (LocalHomeomorph.ofSet s hs).toLocalEquiv.target = s

def LocalHomeomorph.ofSet {α : Type u_1} [TopologicalSpace α] (s : Set α) (hs : IsOpen s) : LocalHomeomorph α α

The identity local equiv on a set s

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LocalHomeomorph.ofSet_toLocalEquiv {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsOpen s) : (LocalHomeomorph.ofSet s hs).toLocalEquiv = LocalEquiv.ofSet s

@[simp]

theorem LocalHomeomorph.ofSet_symm {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsOpen s) : LocalHomeomorph.symm (LocalHomeomorph.ofSet s hs) = LocalHomeomorph.ofSet s hs

@[simp]

theorem LocalHomeomorph.ofSet_univ_eq_refl {α : Type u_1} [TopologicalSpace α] : LocalHomeomorph.ofSet Set.univ (_ : IsOpen Set.univ) = LocalHomeomorph.refl α

@[simp]

theorem LocalHomeomorph.trans'_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) (h : e.target = e'.source) : ∀ (a : α), ↑(LocalHomeomorph.trans' e e' h) a = ↑e' (↑e a)

@[simp]

theorem LocalHomeomorph.trans'_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) (h : e.target = e'.source) : ∀ (a : γ), ↑(LocalHomeomorph.symm (LocalHomeomorph.trans' e e' h)) a = ↑(LocalHomeomorph.symm e) (↑(LocalHomeomorph.symm e') a)

@[simp]

theorem LocalHomeomorph.trans'_toLocalEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) (h : e.target = e'.source) : (LocalHomeomorph.trans' e e' h).toLocalEquiv = LocalEquiv.trans' e.toLocalEquiv e'.toLocalEquiv h

theorem LocalHomeomorph.trans'_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) (h : e.target = e'.source) : (LocalHomeomorph.trans' e e' h).toLocalEquiv.target = e'.target

theorem LocalHomeomorph.trans'_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) (h : e.target = e'.source) : (LocalHomeomorph.trans' e e' h).toLocalEquiv.source = e.source

def LocalHomeomorph.trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) (h : e.target = e'.source) : LocalHomeomorph α γ

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

Equations

• One or more equations did not get rendered due to their size.

def LocalHomeomorph.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : LocalHomeomorph α γ

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LocalHomeomorph.trans_toLocalEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : (LocalHomeomorph.trans e e').toLocalEquiv = LocalEquiv.trans e.toLocalEquiv e'.toLocalEquiv

@[simp]

theorem LocalHomeomorph.coe_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : ↑(LocalHomeomorph.trans e e') = ↑e' ∘ ↑e

@[simp]

theorem LocalHomeomorph.coe_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : ↑(LocalHomeomorph.symm (LocalHomeomorph.trans e e')) = ↑(LocalHomeomorph.symm e) ∘ ↑(LocalHomeomorph.symm e')

theorem LocalHomeomorph.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) {x : α} : ↑(LocalHomeomorph.trans e e') x = ↑e' (↑e x)

theorem LocalHomeomorph.trans_symm_eq_symm_trans_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : LocalHomeomorph.symm (LocalHomeomorph.trans e e') = LocalHomeomorph.trans (LocalHomeomorph.symm e') (LocalHomeomorph.symm e)

theorem LocalHomeomorph.trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : (LocalHomeomorph.trans e e').toLocalEquiv.source = e.source ∩ ↑e ⁻¹' e'.source

theorem LocalHomeomorph.trans_source' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : (LocalHomeomorph.trans e e').toLocalEquiv.source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)

theorem LocalHomeomorph.trans_source'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : (LocalHomeomorph.trans e e').toLocalEquiv.source = ↑(LocalHomeomorph.symm e) '' (e.target ∩ e'.source)

theorem LocalHomeomorph.image_trans_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : ↑e '' (LocalHomeomorph.trans e e').toLocalEquiv.source = e.target ∩ e'.source

theorem LocalHomeomorph.trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : (LocalHomeomorph.trans e e').toLocalEquiv.target = e'.target ∩ ↑(LocalHomeomorph.symm e') ⁻¹' e.target

theorem LocalHomeomorph.trans_target' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : (LocalHomeomorph.trans e e').toLocalEquiv.target = e'.target ∩ ↑(LocalHomeomorph.symm e') ⁻¹' (e'.source ∩ e.target)

theorem LocalHomeomorph.trans_target'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : (LocalHomeomorph.trans e e').toLocalEquiv.target = ↑e' '' (e'.source ∩ e.target)

theorem LocalHomeomorph.inv_image_trans_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) : ↑(LocalHomeomorph.symm e') '' (LocalHomeomorph.trans e e').toLocalEquiv.target = e'.source ∩ e.target

theorem LocalHomeomorph.trans_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) (e'' : LocalHomeomorph γ δ) : LocalHomeomorph.trans (LocalHomeomorph.trans e e') e'' = LocalHomeomorph.trans e (LocalHomeomorph.trans e' e'')

@[simp]

theorem LocalHomeomorph.trans_refl {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : LocalHomeomorph.trans e (LocalHomeomorph.refl β) = e

@[simp]

theorem LocalHomeomorph.refl_trans {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : LocalHomeomorph.trans (LocalHomeomorph.refl α) e = e

theorem LocalHomeomorph.trans_ofSet {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set β} (hs : IsOpen s) : LocalHomeomorph.trans e (LocalHomeomorph.ofSet s hs) = LocalHomeomorph.restr e (↑e ⁻¹' s)

theorem LocalHomeomorph.trans_of_set' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set β} (hs : IsOpen s) : LocalHomeomorph.trans e (LocalHomeomorph.ofSet s hs) = LocalHomeomorph.restr e (e.source ∩ ↑e ⁻¹' s)

theorem LocalHomeomorph.ofSet_trans {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set α} (hs : IsOpen s) : LocalHomeomorph.trans (LocalHomeomorph.ofSet s hs) e = LocalHomeomorph.restr e s

theorem LocalHomeomorph.ofSet_trans' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set α} (hs : IsOpen s) : LocalHomeomorph.trans (LocalHomeomorph.ofSet s hs) e = LocalHomeomorph.restr e (e.source ∩ s)

@[simp]

theorem LocalHomeomorph.ofSet_trans_ofSet {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsOpen s) {s' : Set α} (hs' : IsOpen s') : LocalHomeomorph.trans (LocalHomeomorph.ofSet s hs) (LocalHomeomorph.ofSet s' hs') = LocalHomeomorph.ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))

theorem LocalHomeomorph.restr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph β γ) (s : Set α) : LocalHomeomorph.trans (LocalHomeomorph.restr e s) e' = LocalHomeomorph.restr (LocalHomeomorph.trans e e') s

@[simp]

theorem LocalHomeomorph.transHomeomorph_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : β ≃ₜ γ) : ↑(LocalHomeomorph.transHomeomorph e e') = ↑e' ∘ ↑e

@[simp]

theorem LocalHomeomorph.transHomeomorph_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : β ≃ₜ γ) : (LocalHomeomorph.transHomeomorph e e').toLocalEquiv.source = e.source

@[simp]

theorem LocalHomeomorph.transHomeomorph_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : β ≃ₜ γ) : ↑(LocalHomeomorph.symm (LocalHomeomorph.transHomeomorph e e')) = ↑(LocalHomeomorph.symm e) ∘ ↑(Homeomorph.symm e')

@[simp]

theorem LocalHomeomorph.transHomeomorph_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : β ≃ₜ γ) : (LocalHomeomorph.transHomeomorph e e').toLocalEquiv.target = ↑(Homeomorph.symm e') ⁻¹' e.target

def LocalHomeomorph.transHomeomorph {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : β ≃ₜ γ) : LocalHomeomorph α γ

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

Equations

• One or more equations did not get rendered due to their size.

theorem LocalHomeomorph.transHomeomorph_eq_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) (e' : β ≃ₜ γ) : LocalHomeomorph.transHomeomorph e e' = LocalHomeomorph.trans e (Homeomorph.toLocalHomeomorph e')

@[simp]

theorem Homeomorph.transLocalHomeomorph_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e' : LocalHomeomorph β γ) (e : α ≃ₜ β) : (Homeomorph.transLocalHomeomorph e' e).toLocalEquiv.target = e'.target

@[simp]

theorem Homeomorph.transLocalHomeomorph_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e' : LocalHomeomorph β γ) (e : α ≃ₜ β) : ↑(LocalHomeomorph.symm (Homeomorph.transLocalHomeomorph e' e)) = ↑(Homeomorph.symm e) ∘ ↑(LocalHomeomorph.symm e')

@[simp]

theorem Homeomorph.transLocalHomeomorph_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e' : LocalHomeomorph β γ) (e : α ≃ₜ β) : ↑(Homeomorph.transLocalHomeomorph e' e) = ↑e' ∘ ↑e

@[simp]

theorem Homeomorph.transLocalHomeomorph_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e' : LocalHomeomorph β γ) (e : α ≃ₜ β) : (Homeomorph.transLocalHomeomorph e' e).toLocalEquiv.source = ↑e ⁻¹' e'.source

def Homeomorph.transLocalHomeomorph {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e' : LocalHomeomorph β γ) (e : α ≃ₜ β) : LocalHomeomorph α γ

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

Equations

• One or more equations did not get rendered due to their size.

theorem Homeomorph.transLocalHomeomorph_eq_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e' : LocalHomeomorph β γ) (e : α ≃ₜ β) : Homeomorph.transLocalHomeomorph e' e = LocalHomeomorph.trans (Homeomorph.toLocalHomeomorph e) e'

def LocalHomeomorph.EqOnSource {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalHomeomorph α β) : Prop

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

Equations

• LocalHomeomorph.EqOnSource e e' = (e.source = e'.source ∧ Set.EqOn (↑e) (↑e') e.source)

theorem LocalHomeomorph.eqOnSource_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalHomeomorph α β) : LocalHomeomorph.EqOnSource e e' ↔ LocalEquiv.EqOnSource e.toLocalEquiv e'.toLocalEquiv

instance LocalHomeomorph.eqOnSourceSetoid {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : Setoid (LocalHomeomorph α β)

EqOnSource is an equivalence relation

Equations

• LocalHomeomorph.eqOnSourceSetoid = let src := Setoid.comap LocalHomeomorph.toLocalEquiv LocalEquiv.eqOnSourceSetoid; { r := LocalHomeomorph.EqOnSource, iseqv := (_ : Equivalence Setoid.r) }

theorem LocalHomeomorph.eqOnSource_refl {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : e ≈ e

theorem LocalHomeomorph.EqOnSource.symm' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} (h : e ≈ e') : LocalHomeomorph.symm e ≈ LocalHomeomorph.symm e'

If two local homeomorphisms are equivalent, so are their inverses

theorem LocalHomeomorph.EqOnSource.source_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} (h : e ≈ e') : e.source = e'.source

Two equivalent local homeomorphisms have the same source

theorem LocalHomeomorph.EqOnSource.target_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} (h : e ≈ e') : e.target = e'.target

Two equivalent local homeomorphisms have the same target

theorem LocalHomeomorph.EqOnSource.eqOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} (h : e ≈ e') : Set.EqOn (↑e) (↑e') e.source

Two equivalent local homeomorphisms have coinciding toFun on the source

theorem LocalHomeomorph.EqOnSource.symm_eqOn_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} (h : e ≈ e') : Set.EqOn (↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e')) e.target

Two equivalent local homeomorphisms have coinciding invFun on the target

theorem LocalHomeomorph.EqOnSource.trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} {f : LocalHomeomorph β γ} {f' : LocalHomeomorph β γ} (he : e ≈ e') (hf : f ≈ f') : LocalHomeomorph.trans e f ≈ LocalHomeomorph.trans e' f'

Composition of local homeomorphisms respects equivalence

theorem LocalHomeomorph.EqOnSource.restr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} (he : e ≈ e') (s : Set α) : LocalHomeomorph.restr e s ≈ LocalHomeomorph.restr e' s

Restriction of local homeomorphisms respects equivalence

theorem LocalHomeomorph.Set.EqOn.restr_eqOn_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} (h : Set.EqOn (↑e) (↑e') (e.source ∩ e'.source)) : LocalHomeomorph.restr e e'.source ≈ LocalHomeomorph.restr e' e.source

theorem LocalHomeomorph.trans_self_symm {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : LocalHomeomorph.trans e (LocalHomeomorph.symm e) ≈ LocalHomeomorph.ofSet e.source (_ : IsOpen e.source)

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

theorem LocalHomeomorph.trans_symm_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : LocalHomeomorph.trans (LocalHomeomorph.symm e) e ≈ LocalHomeomorph.ofSet e.target (_ : IsOpen e.target)

theorem LocalHomeomorph.eq_of_eq_on_source_univ {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : LocalHomeomorph α β} {e' : LocalHomeomorph α β} (h : e ≈ e') (s : e.source = Set.univ) (t : e.target = Set.univ) : e = e'

@[simp]

theorem LocalHomeomorph.prod_toLocalEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph γ δ) : (LocalHomeomorph.prod e e').toLocalEquiv = LocalEquiv.prod e.toLocalEquiv e'.toLocalEquiv

@[simp]

theorem LocalHomeomorph.prod_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph γ δ) : ↑(LocalHomeomorph.prod e e') = fun p => (↑e p.fst, ↑e' p.snd)

theorem LocalHomeomorph.prod_target {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph γ δ) : (LocalHomeomorph.prod e e').toLocalEquiv.target = e.target ×ˢ e'.target

theorem LocalHomeomorph.prod_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph γ δ) (p : β × δ) : ↑(LocalHomeomorph.symm (LocalHomeomorph.prod e e')) p = (↑(LocalHomeomorph.symm e) p.fst, ↑(LocalHomeomorph.symm e') p.snd)

theorem LocalHomeomorph.prod_source {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph γ δ) : (LocalHomeomorph.prod e e').toLocalEquiv.source = e.source ×ˢ e'.source

def LocalHomeomorph.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph γ δ) : LocalHomeomorph (α × γ) (β × δ)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LocalHomeomorph.prod_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] (e : LocalHomeomorph α β) (e' : LocalHomeomorph γ δ) : LocalHomeomorph.symm (LocalHomeomorph.prod e e') = LocalHomeomorph.prod (LocalHomeomorph.symm e) (LocalHomeomorph.symm e')

@[simp]

theorem LocalHomeomorph.refl_prod_refl {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] : LocalHomeomorph.prod (LocalHomeomorph.refl α) (LocalHomeomorph.refl β) = LocalHomeomorph.refl (α × β)

@[simp]

theorem LocalHomeomorph.prod_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {η : Type u_5} {ε : Type u_6} [TopologicalSpace η] [TopologicalSpace ε] (e : LocalHomeomorph α β) (f : LocalHomeomorph β γ) (e' : LocalHomeomorph δ η) (f' : LocalHomeomorph η ε) : LocalHomeomorph.trans (LocalHomeomorph.prod e e') (LocalHomeomorph.prod f f') = LocalHomeomorph.prod (LocalHomeomorph.trans e f) (LocalHomeomorph.trans e' f')

theorem LocalHomeomorph.prod_eq_prod_of_nonempty {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {e₁ : LocalHomeomorph α β} {e₁' : LocalHomeomorph α β} {e₂ : LocalHomeomorph γ δ} {e₂' : LocalHomeomorph γ δ} (h : Set.Nonempty (LocalHomeomorph.prod e₁ e₂).toLocalEquiv.source) : LocalHomeomorph.prod e₁ e₂ = LocalHomeomorph.prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'

theorem LocalHomeomorph.prod_eq_prod_of_nonempty' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {e₁ : LocalHomeomorph α β} {e₁' : LocalHomeomorph α β} {e₂ : LocalHomeomorph γ δ} {e₂' : LocalHomeomorph γ δ} (h : Set.Nonempty (LocalHomeomorph.prod e₁' e₂').toLocalEquiv.source) : LocalHomeomorph.prod e₁ e₂ = LocalHomeomorph.prod e₁' e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'

@[simp]

theorem LocalHomeomorph.piecewise_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalHomeomorph α β) (s : Set α) (t : Set β) [(x : α) → Decidable (x ∈ s)] [(y : β) → Decidable (y ∈ t)] (H : LocalHomeomorph.IsImage e s t) (H' : LocalHomeomorph.IsImage e' s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : ↑(LocalHomeomorph.piecewise e e' s t H H' Hs Heq) = Set.piecewise s ↑e ↑e'

@[simp]

theorem LocalHomeomorph.piecewise_toLocalEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalHomeomorph α β) (s : Set α) (t : Set β) [(x : α) → Decidable (x ∈ s)] [(y : β) → Decidable (y ∈ t)] (H : LocalHomeomorph.IsImage e s t) (H' : LocalHomeomorph.IsImage e' s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : (LocalHomeomorph.piecewise e e' s t H H' Hs Heq).toLocalEquiv = LocalEquiv.piecewise e.toLocalEquiv e'.toLocalEquiv s t H H'

def LocalHomeomorph.piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalHomeomorph α β) (s : Set α) (t : Set β) [(x : α) → Decidable (x ∈ s)] [(y : β) → Decidable (y ∈ t)] (H : LocalHomeomorph.IsImage e s t) (H' : LocalHomeomorph.IsImage e' s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : LocalHomeomorph α β

Combine two LocalHomeomorphs using Set.piecewise. The source of the new LocalHomeomorph 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 toFun and invFun 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem LocalHomeomorph.symm_piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalHomeomorph α β) {s : Set α} {t : Set β} [(x : α) → Decidable (x ∈ s)] [(y : β) → Decidable (y ∈ t)] (H : LocalHomeomorph.IsImage e s t) (H' : LocalHomeomorph.IsImage e' s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : LocalHomeomorph.symm (LocalHomeomorph.piecewise e e' s t H H' Hs Heq) = LocalHomeomorph.piecewise (LocalHomeomorph.symm e) (LocalHomeomorph.symm e') t s (_ : LocalHomeomorph.IsImage (LocalHomeomorph.symm e) t s) (_ : LocalHomeomorph.IsImage (LocalHomeomorph.symm e') t s) (_ : e.target ∩ frontier t = e'.target ∩ frontier t) (_ : Set.EqOn (↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e')) (e.target ∩ frontier t))

def LocalHomeomorph.disjointUnion {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (e' : LocalHomeomorph α β) [(x : α) → Decidable (x ∈ e.source)] [(y : β) → Decidable (y ∈ e.target)] (Hs : Disjoint e.source e'.source) (Ht : Disjoint e.target e'.target) : LocalHomeomorph α β

Combine two LocalHomeomorphs with disjoint sources and disjoint targets. We reuse LocalHomeomorph.piecewise then override toLocalEquiv to LocalEquiv.disjointUnion. This way we have better definitional equalities for source and target.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LocalHomeomorph.pi_toLocalEquiv {ι : Type u_5} [Fintype ι] {Xi : ι → Type u_6} {Yi : ι → Type u_7} [(i : ι) → TopologicalSpace (Xi i)] [(i : ι) → TopologicalSpace (Yi i)] (ei : (i : ι) → LocalHomeomorph (Xi i) (Yi i)) : (LocalHomeomorph.pi ei).toLocalEquiv = LocalEquiv.pi fun i => (ei i).toLocalEquiv

def LocalHomeomorph.pi {ι : Type u_5} [Fintype ι] {Xi : ι → Type u_6} {Yi : ι → Type u_7} [(i : ι) → TopologicalSpace (Xi i)] [(i : ι) → TopologicalSpace (Yi i)] (ei : (i : ι) → LocalHomeomorph (Xi i) (Yi i)) : LocalHomeomorph ((i : ι) → Xi i) ((i : ι) → Yi i)

The product of a finite family of LocalHomeomorphs.

Equations

• One or more equations did not get rendered due to their size.

theorem LocalHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) {f : β → γ} {s : Set β} {x : β} (h : x ∈ e.target) : ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑(LocalHomeomorph.symm e) 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 LocalHomeomorph.continuousAt_iff_continuousAt_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) {f : β → γ} {x : β} (h : x ∈ e.target) : ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) x)

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

theorem LocalHomeomorph.continuousOn_iff_continuousOn_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) {f : β → γ} {s : Set β} (h : s ⊆ e.target) : ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.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 LocalHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) {f : γ → α} {s : Set γ} {x : γ} (hx : f x ∈ e.source) (h : f ⁻¹' e.source ∈ nhdsWithin x s) : ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑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 LocalHomeomorph.continuousAt_iff_continuousAt_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) {f : γ → α} {x : γ} (h : f ⁻¹' e.source ∈ nhds x) : ContinuousAt f x ↔ ContinuousAt (↑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 LocalHomeomorph.continuousOn_iff_continuousOn_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) {f : γ → α} {s : Set γ} (h : s ⊆ f ⁻¹' e.source) : ContinuousOn f s ↔ ContinuousOn (↑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 LocalHomeomorph.continuous_iff_continuous_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : LocalHomeomorph α β) {f : γ → α} (h : f ⁻¹' e.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.

@[simp]

theorem LocalHomeomorph.homeomorphOfImageSubsetSource_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set α} {t : Set β} (hs : s ⊆ e.source) (ht : ↑e '' s = t) : ∀ (a : ↑s), ↑(LocalHomeomorph.homeomorphOfImageSubsetSource e hs ht) a = Set.MapsTo.restrict (↑e) s t (_ : Set.MapsTo (↑e) s t) a

@[simp]

theorem LocalHomeomorph.homeomorphOfImageSubsetSource_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set α} {t : Set β} (hs : s ⊆ e.source) (ht : ↑e '' s = t) : ∀ (a : ↑t), ↑(Homeomorph.symm (LocalHomeomorph.homeomorphOfImageSubsetSource e hs ht)) a = Set.MapsTo.restrict (↑(LocalHomeomorph.symm e)) t s (_ : ∀ (y : β), y ∈ t → ↑(LocalHomeomorph.symm e) y ∈ s) a

def LocalHomeomorph.homeomorphOfImageSubsetSource {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : Set α} {t : Set β} (hs : s ⊆ e.source) (ht : ↑e '' s = t) : ↑s ≃ₜ ↑t

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LocalHomeomorph.toHomeomorphSourceTarget_symm_apply_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : ∀ (a : ↑e.target), ↑(↑(Homeomorph.symm (LocalHomeomorph.toHomeomorphSourceTarget e)) a) = ↑(LocalHomeomorph.symm e) ↑a

@[simp]

theorem LocalHomeomorph.toHomeomorphSourceTarget_apply_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : ∀ (a : ↑e.source), ↑(↑(LocalHomeomorph.toHomeomorphSourceTarget e) a) = ↑e ↑a

def LocalHomeomorph.toHomeomorphSourceTarget {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) : ↑e.source ≃ₜ ↑e.target

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

Equations

• LocalHomeomorph.toHomeomorphSourceTarget e = LocalHomeomorph.homeomorphOfImageSubsetSource e (_ : e.source ⊆ e.source) (_ : ↑e '' e.source = e.target)

theorem LocalHomeomorph.secondCountableTopology_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace.SecondCountableTopology β] (e : LocalHomeomorph α β) : TopologicalSpace.SecondCountableTopology ↑e.source

theorem LocalHomeomorph.nhds_eq_comap_inf_principal {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {x : α} (hx : x ∈ e.source) : nhds x = Filter.comap (↑e) (nhds (↑e x)) ⊓ Filter.principal e.source

@[simp]

theorem LocalHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (h : e.source = Set.univ) (h' : e.target = Set.univ) : ↑(LocalHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv e h h') = ↑e

@[simp]

theorem LocalHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (h : e.source = Set.univ) (h' : e.target = Set.univ) : ↑(Homeomorph.symm (LocalHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv e h h')) = ↑(LocalHomeomorph.symm e)

def LocalHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (h : e.source = Set.univ) (h' : e.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

• One or more equations did not get rendered due to their size.

theorem LocalHomeomorph.to_openEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (h : e.source = Set.univ) : OpenEmbedding ↑e

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

@[simp]

theorem Homeomorph.refl_toLocalHomeomorph {α : Type u_1} [TopologicalSpace α] : Homeomorph.toLocalHomeomorph (Homeomorph.refl α) = LocalHomeomorph.refl α

@[simp]

theorem Homeomorph.symm_toLocalHomeomorph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : α ≃ₜ β) : Homeomorph.toLocalHomeomorph (Homeomorph.symm e) = LocalHomeomorph.symm (Homeomorph.toLocalHomeomorph e)

@[simp]

theorem Homeomorph.trans_toLocalHomeomorph {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (e : α ≃ₜ β) (e' : β ≃ₜ γ) : Homeomorph.toLocalHomeomorph (Homeomorph.trans e e') = LocalHomeomorph.trans (Homeomorph.toLocalHomeomorph e) (Homeomorph.toLocalHomeomorph e')

@[simp]

theorem OpenEmbedding.toLocalHomeomorph_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (h : OpenEmbedding f) [Nonempty α] : ↑(OpenEmbedding.toLocalHomeomorph f h) = f

@[simp]

theorem OpenEmbedding.toLocalHomeomorph_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (h : OpenEmbedding f) [Nonempty α] : (OpenEmbedding.toLocalHomeomorph f h).toLocalEquiv.target = Set.range f

@[simp]

theorem OpenEmbedding.toLocalHomeomorph_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (h : OpenEmbedding f) [Nonempty α] : (OpenEmbedding.toLocalHomeomorph f h).toLocalEquiv.source = Set.univ

noncomputable def OpenEmbedding.toLocalHomeomorph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (h : OpenEmbedding f) [Nonempty α] : LocalHomeomorph α β

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

Equations

• One or more equations did not get rendered due to their size.

theorem OpenEmbedding.continuousAt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : β → γ} (hf : OpenEmbedding f) {x : α} : ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

noncomputable def TopologicalSpace.Opens.localHomeomorphSubtypeCoe {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Opens α) [Nonempty { x // x ∈ s }] : LocalHomeomorph { x // x ∈ s } α

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

Equations

• TopologicalSpace.Opens.localHomeomorphSubtypeCoe s = OpenEmbedding.toLocalHomeomorph Subtype.val (_ : OpenEmbedding Subtype.val)

@[simp]

theorem TopologicalSpace.Opens.localHomeomorphSubtypeCoe_coe {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Opens α) [Nonempty { x // x ∈ s }] : ↑(TopologicalSpace.Opens.localHomeomorphSubtypeCoe s) = Subtype.val

@[simp]

theorem TopologicalSpace.Opens.localHomeomorphSubtypeCoe_source {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Opens α) [Nonempty { x // x ∈ s }] : (TopologicalSpace.Opens.localHomeomorphSubtypeCoe s).toLocalEquiv.source = Set.univ

@[simp]

theorem TopologicalSpace.Opens.localHomeomorphSubtypeCoe_target {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Opens α) [Nonempty { x // x ∈ s }] : (TopologicalSpace.Opens.localHomeomorphSubtypeCoe s).toLocalEquiv.target = ↑s

noncomputable def LocalHomeomorph.subtypeRestr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : TopologicalSpace.Opens α) [Nonempty { x // x ∈ s }] : LocalHomeomorph { x // x ∈ 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

• LocalHomeomorph.subtypeRestr e s = LocalHomeomorph.trans (TopologicalSpace.Opens.localHomeomorphSubtypeCoe s) e

theorem LocalHomeomorph.subtypeRestr_def {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : TopologicalSpace.Opens α) [Nonempty { x // x ∈ s }] : LocalHomeomorph.subtypeRestr e s = LocalHomeomorph.trans (TopologicalSpace.Opens.localHomeomorphSubtypeCoe s) e

@[simp]

theorem LocalHomeomorph.subtypeRestr_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : TopologicalSpace.Opens α) [Nonempty { x // x ∈ s }] : ↑(LocalHomeomorph.subtypeRestr e s) = Set.restrict ↑s ↑e

@[simp]

theorem LocalHomeomorph.subtypeRestr_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) (s : TopologicalSpace.Opens α) [Nonempty { x // x ∈ s }] : (LocalHomeomorph.subtypeRestr e s).toLocalEquiv.source = Subtype.val ⁻¹' e.source

theorem LocalHomeomorph.map_subtype_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {s : TopologicalSpace.Opens α} [Nonempty { x // x ∈ s }] {x : { x // x ∈ s }} (hxe : ↑x ∈ e.source) : ↑e ↑x ∈ (LocalHomeomorph.subtypeRestr e s).toLocalEquiv.target

theorem LocalHomeomorph.subtypeRestr_symm_trans_subtypeRestr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : TopologicalSpace.Opens α) [Nonempty { x // x ∈ s }] (f : LocalHomeomorph α β) (f' : LocalHomeomorph α β) : LocalHomeomorph.trans (LocalHomeomorph.symm (LocalHomeomorph.subtypeRestr f s)) (LocalHomeomorph.subtypeRestr f' s) ≈ LocalHomeomorph.restr (LocalHomeomorph.trans (LocalHomeomorph.symm f) f') (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' ↑s)

theorem LocalHomeomorph.subtypeRestr_symm_eqOn_of_le {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (e : LocalHomeomorph α β) {U : TopologicalSpace.Opens α} {V : TopologicalSpace.Opens α} [Nonempty { x // x ∈ U }] [Nonempty { x // x ∈ V }] (hUV : U ≤ V) : Set.EqOn (↑(LocalHomeomorph.symm (LocalHomeomorph.subtypeRestr e V))) (Set.inclusion hUV ∘ ↑(LocalHomeomorph.symm (LocalHomeomorph.subtypeRestr e U))) (LocalHomeomorph.subtypeRestr e U).toLocalEquiv.target