We define the subtype of open sets in a topological space.
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 (λ (Us : set (topological_space.opens α)), ⟨⋃₀(coe '' Us), _⟩) topological_space.opens.complete_lattice._proof_9 complete_lattice.Inf topological_space.opens.complete_lattice._proof_10
The preimage of an open set, as an open set.
A homeomorphism induces an equivalence on open sets, by taking comaps.