Open sets #
Summary #
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 x
is the type of open subsets of a topological spaceα
containingx : α
.
The type of open subsets of a topological space.
Equations
- topological_space.opens α = {s // is_open s}
Instances for topological_space.opens
- topological_space.opens.set.has_coe
- topological_space.opens.has_subset
- topological_space.opens.has_mem
- topological_space.opens.partial_order
- topological_space.opens.complete_lattice
- topological_space.opens.has_inter
- topological_space.opens.has_union
- topological_space.opens.has_emptyc
- topological_space.opens.inhabited
- topological_space.opens.order.frame
- topological_space.opens.finite
- open_subgroup.has_coe_opens
- open_add_subgroup.has_coe_opens
Equations
- topological_space.opens.set.has_coe = {coe := subtype.val (λ (s : set α), is_open s)}
the coercion opens α → set α
applied to a pair is the same as taking the first component
Equations
- topological_space.opens.has_subset = {subset := λ (U V : topological_space.opens α), ↑U ⊆ ↑V}
Equations
- topological_space.opens.has_mem = {mem := λ (a : α) (U : topological_space.opens α), a ∈ ↑U}
Equations
- topological_space.opens.partial_order = subtype.partial_order (λ (s : set α), is_open s)
The interior of a set, as an element of opens
.
Equations
The galois coinsertion between sets and opens.
Equations
- topological_space.opens.complete_lattice = topological_space.opens.gi.lift_complete_lattice.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 (λ (S : set (topological_space.opens α)), ⟨⋃ (s : topological_space.opens α) (H : s ∈ S), ↑s, _⟩) topological_space.opens.complete_lattice._proof_9 complete_lattice.Inf topological_space.opens.complete_lattice._proof_10
Equations
- topological_space.opens.has_inter = {inter := λ (U V : topological_space.opens α), U ⊓ V}
Equations
- topological_space.opens.has_union = {union := λ (U V : topological_space.opens α), U ⊔ V}
Equations
Equations
Equations
- topological_space.opens.order.frame = {sup := complete_lattice.sup topological_space.opens.complete_lattice, le := complete_lattice.le topological_space.opens.complete_lattice, lt := complete_lattice.lt topological_space.opens.complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf topological_space.opens.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup (conditionally_complete_lattice.to_has_Sup (topological_space.opens α)), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf topological_space.opens.complete_lattice, Inf_le := _, le_Inf := _, top := complete_lattice.top topological_space.opens.complete_lattice, bot := complete_lattice.bot topological_space.opens.complete_lattice, le_top := _, bot_le := _, inf_Sup_le_supr_inf := _}
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.
Equations
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
- topological_space.opens.comap f = {to_inf_top_hom := {to_inf_hom := {to_fun := λ (s : topological_space.opens β), ⟨⇑f ⁻¹' ↑s, _⟩, map_inf' := _}, map_top' := _}, map_Sup' := _}
A homeomorphism induces an equivalence on open sets, by taking comaps.
Equations
- topological_space.opens.equiv f = {to_fun := ⇑(topological_space.opens.comap f.symm.to_continuous_map), inv_fun := ⇑(topological_space.opens.comap f.to_continuous_map), left_inv := _, right_inv := _}
A homeomorphism induces an order isomorphism on open sets, by taking comaps.