Open sets #
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.IsBasisis a predicate saying that a set of
openss form a topological basis.
TopologicalSpace.Opens.comap: preimage of an open set under a continuous map as a
Homeomorph.opensCongr: order-preserving equivalence between open sets in the domain and the codomain of a homeomorphism.
Bundled open neighborhoods #
TopologicalSpace.OpenNhdsOf xis the type of open subsets of a topological space
x : α.
TopologicalSpace.OpenNhdsOf.comap f x Uis the preimage of open neighborhood
f : C(α, β).
Main results #
- Port the
auto_casestactic version (as a plugin if the ported
auto_caseswill allow plugins).
α 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
- carrier : Set α
- is_open' : IsOpen s.carrier
- mem' : x ∈ s.carrier
xbelongs to every
U : TopologicalSpace.OpenNhdsOf x.
Preimage of an open neighborhood of
f x under a continuous map
f as a