topology.opens

# 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 α containing x : α.
def topological_space.opens (α : Type u_1)  :
Type u_1

The type of open subsets of a topological space.

Equations
@[protected, instance]
def topological_space.opens.set.has_coe {α : Type u_1}  :
(set α)
Equations
theorem topological_space.opens.coe_mk {α : Type u_1} {U : set α} {hU : is_open U} :
U, hU⟩ = U

the coercion opens α → set α applied to a pair is the same as taking the first component

@[protected, instance]
def topological_space.opens.has_subset {α : Type u_1}  :
Equations
@[protected, instance]
def topological_space.opens.has_mem {α : Type u_1}  :
Equations
@[simp]
theorem topological_space.opens.subset_coe {α : Type u_1} {U V : topological_space.opens α} :
U V = (U V)
@[simp]
theorem topological_space.opens.mem_coe {α : Type u_1} {x : α} {U : topological_space.opens α} :
x U = (x U)
@[ext]
theorem topological_space.opens.ext {α : Type u_1} {U V : topological_space.opens α} (h : U = V) :
U = V
@[ext]
theorem topological_space.opens.ext_iff {α : Type u_1} {U V : topological_space.opens α} :
U = V U = V
@[protected, instance]
def topological_space.opens.partial_order {α : Type u_1}  :
Equations
def topological_space.opens.interior {α : Type u_1} (s : set α) :

The interior of a set, as an element of opens.

Equations
theorem topological_space.opens.gc {α : Type u_1}  :

The galois insertion between sets and opens, but ordered by reverse inclusion.

Equations
@[simp]
theorem topological_space.opens.gi_choice_val {α : Type u_1} {s : order_dual (set α)}  :
.val = s
@[protected, instance]
Equations
theorem topological_space.opens.le_def {α : Type u_1} {U V : topological_space.opens α} :
U V U V
@[simp]
theorem topological_space.opens.mk_inf_mk {α : Type u_1} {U V : set α} {hU : is_open U} {hV : is_open V} :
U, hU⟩ V, hV⟩ = U V, _⟩
@[simp, norm_cast]
theorem topological_space.opens.coe_inf {α : Type u_1} {U V : topological_space.opens α} :
(U V) = U V
@[simp]
theorem topological_space.opens.coe_bot {α : Type u_1}  :
@[simp]
theorem topological_space.opens.coe_top {α : Type u_1}  :
@[protected, instance]
def topological_space.opens.has_inter {α : Type u_1}  :
Equations
@[protected, instance]
def topological_space.opens.has_union {α : Type u_1}  :
Equations
@[protected, instance]
def topological_space.opens.has_emptyc {α : Type u_1}  :
Equations
@[protected, instance]
def topological_space.opens.inhabited {α : Type u_1}  :
Equations
@[simp]
theorem topological_space.opens.inter_eq {α : Type u_1} (U V : topological_space.opens α) :
U V = U V
@[simp]
theorem topological_space.opens.union_eq {α : Type u_1} (U V : topological_space.opens α) :
U V = U V
@[simp]
theorem topological_space.opens.empty_eq {α : Type u_1}  :
@[simp]
theorem topological_space.opens.Sup_s {α : Type u_1} {Us : set } :
(Sup Us) = ⋃₀(coe '' Us)
theorem topological_space.opens.supr_def {α : Type u_1} {ι : Sort u_2} (s : ι → ) :
(⨆ (i : ι), s i) = ⋃ (i : ι), (s i), _⟩
@[simp]
theorem topological_space.opens.supr_mk {α : Type u_1} {ι : Sort u_2} (s : ι → set α) (h : ∀ (i : ι), is_open (s i)) :
(⨆ (i : ι), s i, _⟩) = ⋃ (i : ι), s i, _⟩
@[simp]
theorem topological_space.opens.supr_s {α : Type u_1} {ι : Sort u_2} (s : ι → ) :
(⨆ (i : ι), s i) = ⋃ (i : ι), (s i)
@[simp]
theorem topological_space.opens.mem_supr {α : Type u_1} {ι : Sort u_2} {x : α} {s : ι → } :
x supr s ∃ (i : ι), x s i
@[simp]
theorem topological_space.opens.mem_Sup {α : Type u_1} {Us : set } {x : α} :
x Sup Us ∃ (u : (H : u Us), x u
theorem topological_space.opens.open_embedding_of_le {α : Type u_1} {U V : topological_space.opens α} (i : U V) :
def topological_space.opens.is_basis {α : Type u_1} (B : set ) :
Prop

A set of opens α is a basis if the set of corresponding sets is a topological basis.

Equations
theorem topological_space.opens.is_basis_iff_nbhd {α : Type u_1} {B : set } :
∀ {U : {x : α}, x U(∃ (U' : (H : U' B), x U' U' U)
theorem topological_space.opens.is_basis_iff_cover {α : Type u_1} {B : set } :
∀ (U : , ∃ (Us : (H : Us B), U = Sup Us
def topological_space.opens.comap {α : Type u_1} {β : Type u_2} (f : C(α, β)) :

The preimage of an open set, as an open set.

Equations
@[simp]
theorem topological_space.opens.comap_id {α : Type u_1}  :
theorem topological_space.opens.comap_mono {α : Type u_1} {β : Type u_2} (f : C(α, β)) {V W : topological_space.opens β} (hVW : V W) :
@[simp]
theorem topological_space.opens.coe_comap {α : Type u_1} {β : Type u_2} (f : C(α, β)) (U : topological_space.opens β) :
@[simp]
theorem topological_space.opens.comap_val {α : Type u_1} {β : Type u_2} (f : C(α, β)) (U : topological_space.opens β) :
@[protected]
theorem topological_space.opens.comap_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : C(β, γ)) (f : C(α, β)) :
@[protected]
theorem topological_space.opens.comap_comap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : C(β, γ)) (f : C(α, β)) (U : topological_space.opens γ) :
= U
@[protected, simp]
def topological_space.opens.equiv {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β) :

A homeomorphism induces an equivalence on open sets, by taking comaps.

Equations
@[protected, simp]
def topological_space.opens.order_iso {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β) :

A homeomorphism induces an order isomorphism on open sets, by taking comaps.

Equations
def topological_space.open_nhds_of {α : Type u_1} (x : α) :
Type u_1

The open neighborhoods of a point. See also opens or nhds.

Equations
@[protected, instance]
def topological_space.open_nhds_of.inhabited {α : Type u_1} (x : α) :
Equations