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 α
(complete_structure
, frame
) and open_nhds_of x
(OrderTop
, DistribLattice
).
TODO #
- Rename
TopologicalSpace.Opens
toOpen
? - Port the
auto_cases
tactic version (as a plugin if the portedauto_cases
will allow plugins).
- carrier : Set α
The underlying set of a bundled
TopologicalSpace.Opens
object. - is_open' : IsOpen s.carrier
The
TopologicalSpace.Opens.carrier _
is an open set.
The type of open subsets of a topological space.
Instances For
the coercion Opens α → Set α
applied to a pair is the same as taking the first component
See Note [custom simps projection].
Instances For
The interior of a set, as an element of Opens
.
Instances For
The galois coinsertion between sets and opens.
Instances For
An open set in the indiscrete topology is either empty or the whole space.
A set of opens α
is a basis if the set of corresponding sets is a topological basis.
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.
Instances For
A homeomorphism induces an order-preserving equivalence on open sets, by taking comaps.
Instances For
- carrier : Set α
- is_open' : IsOpen s.carrier
- mem' : x ∈ s.carrier
The point
x
belongs to everyU : TopologicalSpace.OpenNhdsOf x
.
The open neighborhoods of a point. See also Opens
or nhds
.
Instances For
Preimage of an open neighborhood of f x
under a continuous map f
as a LatticeHom
.