Homeomorphisms #
This file defines homeomorphisms between two topological spaces. They are bijections with both
directions continuous. We denote homeomorphisms with the notation ≃ₜ
.
Main definitions and results #
Homeomorph X Y
: The type of homeomorphisms fromX
toY
. This type can be denoted using the following notation:X ≃ₜ Y
.HomeomorphClass
:HomeomorphClass F A B
states thatF
is a type of homeomorphisms.Homeomorph.symm
: the inverse of a homeomorphismHomeomorph.trans
: composing two homeomorphismsHomeomorphisms are open and closed embeddings, inducing, quotient maps etc.
Homeomorph.homeomorphOfContinuousOpen
: A continuous bijection that is an open map is a homeomorphism.Homeomorph.homeomorphOfUnique
: if bothX
andY
have a unique element, thenX ≃ₜ Y
.Equiv.toHomeomorph
: an equivalence between topological spaces respecting openness is a homeomorphism.IsHomeomorph
: the predicate that a function is a homeomorphism
Homeomorphism between X
and Y
, also called topological isomorphism
- toFun : X → Y
- invFun : Y → X
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- continuous_toFun : Continuous self.toFun
The forward map of a homeomorphism is a continuous function.
- continuous_invFun : Continuous self.invFun
The inverse map of a homeomorphism is a continuous function.
Instances For
Homeomorphism between X
and Y
, also called topological isomorphism
Equations
Instances For
Equations
The unique homeomorphism between two empty types.
Equations
Instances For
Inverse of a homeomorphism.
Equations
Instances For
See Note [custom simps projection]
Equations
Instances For
Identity map as a homeomorphism.
Equations
Instances For
Composition of two homeomorphisms.
Equations
Instances For
Change the homeomorphism f
to make the inverse function definitionally equal to g
.
Equations
Instances For
Alias of Homeomorph.isInducing
.
Alias of Homeomorph.isQuotientMap
.
Alias of Homeomorph.isEmbedding
.
If both X
and Y
have a unique element, then X ≃ₜ Y
.
Equations
Instances For
An equivalence between topological spaces respecting openness is a homeomorphism.
Equations
Instances For
An inducing equiv between topological spaces is a homeomorphism.
Equations
Instances For
Alias of Equiv.toHomeomorphOfIsInducing
.
An inducing equiv between topological spaces is a homeomorphism.
Equations
Instances For
If a bijective map e : X ≃ Y
is continuous and open, then it is a homeomorphism.
Equations
Instances For
Alias of Equiv.toHomeomorphOfContinuousOpen
.
If a bijective map e : X ≃ Y
is continuous and open, then it is a homeomorphism.
Equations
Instances For
Alias of Equiv.toHomeomorphOfContinuousOpen_apply
.
If a bijective map e : X ≃ Y
is continuous and open, then it is a homeomorphism.
Equations
Instances For
Alias of Equiv.toHomeomorphOfContinuousClosed
.
If a bijective map e : X ≃ Y
is continuous and open, then it is a homeomorphism.
Equations
Instances For
HomeomorphClass F A B
states that F
is a type of homeomorphisms.
- map_continuous (f : F) : Continuous ⇑f
- inv_continuous (f : F) : Continuous (EquivLike.inv f)
Instances
Turn an element of a type F
satisfying HomeomorphClass F α β
into an actual
Homeomorph
. This is declared as the default coercion from F
to α ≃ₜ β
.
Equations
Instances For
Equations
Predicate saying that f
is a homeomorphism.
This should be used only when f
is a concrete function whose continuous inverse is not easy to
write down. Otherwise, Homeomorph
should be preferred as it bundles the continuous inverse.
Having both Homeomorph
and IsHomeomorph
is justified by the fact that so many function
properties are unbundled in the topology part of the library, and by the fact that a homeomorphism
is not merely a continuous bijection, that is IsHomeomorph f
is not equivalent to
Continuous f ∧ Bijective f
but to Continuous f ∧ Bijective f ∧ IsOpenMap f
.
- continuous : Continuous f
- isOpenMap : IsOpenMap f
- bijective : Function.Bijective f