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 xis 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}
@[protected, instance]
def
topological_space.opens.set.has_coe
{α : Type u_1}
[topological_space α] :
has_coe (topological_space.opens α) (set α)
Equations
- topological_space.opens.set.has_coe = {coe := subtype.val (λ (s : set α), is_open s)}
theorem
topological_space.opens.val_eq_coe
{α : Type u_1}
[topological_space α]
(U : topological_space.opens α) :
theorem
topological_space.opens.coe_mk
{α : Type u_1}
[topological_space α]
{U : set α}
{hU : is_open U} :
the coercion opens α → set α applied to a pair is the same as taking the first component
@[protected, instance]
Equations
- topological_space.opens.has_subset = {subset := λ (U V : topological_space.opens α), ↑U ⊆ ↑V}
@[protected, instance]
Equations
- topological_space.opens.has_mem = {mem := λ (a : α) (U : topological_space.opens α), a ∈ ↑U}
@[simp]
theorem
topological_space.opens.subset_coe
{α : Type u_1}
[topological_space α]
{U V : topological_space.opens α} :
@[simp]
theorem
topological_space.opens.mem_coe
{α : Type u_1}
[topological_space α]
{x : α}
{U : topological_space.opens α} :
@[ext]
theorem
topological_space.opens.ext
{α : Type u_1}
[topological_space α]
{U V : topological_space.opens α}
(h : ↑U = ↑V) :
U = V
@[ext]
theorem
topological_space.opens.ext_iff
{α : Type u_1}
[topological_space α]
{U V : topological_space.opens α} :
@[protected, instance]
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 insertion between sets and opens, but ordered by reverse inclusion.
Equations
- topological_space.opens.gi = {choice := λ (s : order_dual (set α)) (hs : (topological_space.opens.interior s).val ≤ s), ⟨s, _⟩, gc := _, le_l_u := _, choice_eq := _}
@[simp]
theorem
topological_space.opens.gi_choice_val
{α : Type u_1}
[topological_space α]
{s : order_dual (set α)}
{hs : (topological_space.opens.interior s).val ≤ s} :
(topological_space.opens.gi.choice s hs).val = s
@[protected, instance]
Equations
- 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
theorem
topological_space.opens.le_def
{α : Type u_1}
[topological_space α]
{U V : topological_space.opens α} :
@[simp, norm_cast]
theorem
topological_space.opens.coe_inf
{α : Type u_1}
[topological_space α]
{U V : topological_space.opens α} :
@[protected, instance]
Equations
- topological_space.opens.has_inter = {inter := λ (U V : topological_space.opens α), U ⊓ V}
@[protected, instance]
Equations
- topological_space.opens.has_union = {union := λ (U V : topological_space.opens α), U ⊔ V}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem
topological_space.opens.inter_eq
{α : Type u_1}
[topological_space α]
(U V : topological_space.opens α) :
@[simp]
theorem
topological_space.opens.union_eq
{α : Type u_1}
[topological_space α]
(U V : topological_space.opens α) :
@[simp]
@[simp]
theorem
topological_space.opens.Sup_s
{α : Type u_1}
[topological_space α]
{Us : set (topological_space.opens α)} :
theorem
topological_space.opens.supr_def
{α : Type u_1}
[topological_space α]
{ι : Sort u_2}
(s : ι → topological_space.opens α) :
@[simp]
theorem
topological_space.opens.supr_mk
{α : Type u_1}
[topological_space α]
{ι : Sort u_2}
(s : ι → set α)
(h : ∀ (i : ι), is_open (s i)) :
@[simp]
theorem
topological_space.opens.supr_s
{α : Type u_1}
[topological_space α]
{ι : Sort u_2}
(s : ι → topological_space.opens α) :
@[simp]
theorem
topological_space.opens.mem_supr
{α : Type u_1}
[topological_space α]
{ι : Sort u_2}
{x : α}
{s : ι → topological_space.opens α} :
@[simp]
theorem
topological_space.opens.mem_Sup
{α : Type u_1}
[topological_space α]
{Us : set (topological_space.opens α)}
{x : α} :
theorem
topological_space.opens.open_embedding_of_le
{α : Type u_1}
[topological_space α]
{U V : topological_space.opens α}
(i : U ≤ V) :
def
topological_space.opens.is_basis
{α : Type u_1}
[topological_space α]
(B : set (topological_space.opens α)) :
Prop
Equations
theorem
topological_space.opens.is_basis_iff_nbhd
{α : Type u_1}
[topological_space α]
{B : set (topological_space.opens α)} :
topological_space.opens.is_basis B ↔ ∀ {U : topological_space.opens α} {x : α}, x ∈ U → (∃ (U' : topological_space.opens α) (H : U' ∈ B), x ∈ U' ∧ U' ⊆ U)
theorem
topological_space.opens.is_basis_iff_cover
{α : Type u_1}
[topological_space α]
{B : set (topological_space.opens α)} :
topological_space.opens.is_basis B ↔ ∀ (U : topological_space.opens α), ∃ (Us : set (topological_space.opens α)) (H : Us ⊆ B), U = Sup Us
def
topological_space.opens.comap
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : continuous f)
(V : topological_space.opens β) :
The preimage of an open set, as an open set.
Equations
- topological_space.opens.comap hf V = ⟨f ⁻¹' V.val, _⟩
@[simp]
theorem
topological_space.opens.comap_id
{α : Type u_1}
[topological_space α]
(U : topological_space.opens α) :
theorem
topological_space.opens.comap_mono
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : continuous f)
{V W : topological_space.opens β}
(hVW : V ⊆ W) :
@[simp]
theorem
topological_space.opens.coe_comap
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : continuous f)
(U : topological_space.opens β) :
↑(topological_space.opens.comap hf U) = f ⁻¹' ↑U
@[simp]
theorem
topological_space.opens.comap_val
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : continuous f)
(U : topological_space.opens β) :
(topological_space.opens.comap hf U).val = f ⁻¹' ↑U
@[protected]
theorem
topological_space.opens.comap_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{g : β → γ}
{f : α → β}
(hg : continuous g)
(hf : continuous f)
(U : topological_space.opens γ) :
@[protected, simp]
def
topological_space.opens.equiv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α ≃ₜ β) :
A homeomorphism induces an equivalence on open sets, by taking comaps.
Equations
- topological_space.opens.equiv f = {to_fun := topological_space.opens.comap _, inv_fun := topological_space.opens.comap _, left_inv := _, right_inv := _}
@[protected, instance]