Open sets #
We define the subtype of open sets in a topological space.
Main Definitions #
opens αis the type of open subsets of a topological space
open_nhds_of xis the type of open subsets of a topological space
x : α.
The galois insertion between sets and opens, but ordered by reverse inclusion.
- topological_space.opens.complete_lattice = (order_dual.complete_lattice (order_dual (topological_space.opens α))).copy (λ (U V : topological_space.opens α), U ⊆ V) topological_space.opens.complete_lattice._proof_1 ⟨set.univ α, _⟩ topological_space.opens.complete_lattice._proof_2 ⟨∅, _⟩ topological_space.opens.complete_lattice._proof_3 (λ (U V : topological_space.opens α), ⟨↑U ∪ ↑V, _⟩) topological_space.opens.complete_lattice._proof_5 (λ (U V : topological_space.opens α), ⟨↑U ∩ ↑V, _⟩) topological_space.opens.complete_lattice._proof_7 complete_lattice.Sup topological_space.opens.complete_lattice._proof_8 complete_lattice.Inf topological_space.opens.complete_lattice._proof_9
A set of
opens α is a basis if the set of corresponding sets is a topological basis.
The preimage of an open set, as an open set.
A homeomorphism induces an equivalence on open sets, by taking comaps.