Open sets #
Summary #
We define the subtype of open sets in a topological space.
Main Definitions #
Bundled open sets #
TopologicalSpace.Opens α
is the type of open subsets of a topological spaceα
.TopologicalSpace.Opens.IsBasis
is a predicate saying that a set ofOpens
s form a topological basis.TopologicalSpace.Opens.comap
: preimage of an open set under a continuous map as aFrameHom
.Homeomorph.opensCongr
: order-preserving equivalence between open sets in the domain and the codomain of a homeomorphism.
Bundled open neighborhoods #
TopologicalSpace.OpenNhdsOf x
is the type of open subsets of a topological spaceα
containingx : α
.TopologicalSpace.OpenNhdsOf.comap f x U
is the preimage of open neighborhoodU
off x
underf : C(α, β)
.
Main results #
We define order structures on both Opens α
(CompleteLattice
, Frame
) and OpenNhdsOf x
(OrderTop
, DistribLattice
).
TODO #
- Rename
TopologicalSpace.Opens
toOpen
? - Port the
auto_cases
tactic version (as a plugin if the portedauto_cases
will allow plugins).
The type of open subsets of a topological space.
- carrier : Set α
The underlying set of a bundled
TopologicalSpace.Opens
object. The
TopologicalSpace.Opens.carrier _
is an open set.
Instances For
Equations
A version of Set.inclusion
not requiring definitional abuse
Equations
Instances For
See Note [custom simps projection].
Equations
Instances For
The galois coinsertion between sets and opens.
Equations
Instances For
Equations
Equations
Equations
Open sets in a topological space form a frame.
Equations
Instances For
Equations
A set of opens α
is a basis if the set of corresponding sets is a topological basis.
Equations
Instances For
If α
has a basis consisting of compact opens, then an open set in α
is compact open iff
it is a finite union of some elements in the basis
The preimage of an open set, as an open set.
Equations
Instances For
A homeomorphism induces an order-preserving equivalence on open sets, by taking comaps.
Equations
Instances For
The open neighborhoods of a point. See also Opens
or nhds
.
The point
x
belongs to everyU : TopologicalSpace.OpenNhdsOf x
.
Instances For
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Preimage of an open neighborhood of f x
under a continuous map f
as a LatticeHom
.