mathlib documentation

topology.opens

Open sets

Summary

We define the subtype of open sets in a topological space.

Main Definitions

def topological_space.opens (α : Type u_1) [topological_space α] :
Type u_1

The type of open subsets of a topological space.

Equations
theorem topological_space.opens.coe_mk {α : Type u_1} [topological_space α] {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

@[simp]
theorem topological_space.opens.subset_coe {α : Type u_1} [topological_space α] {U V : topological_space.opens α} :
U V = (U V)

@[simp]
theorem topological_space.opens.mem_coe {α : Type u_1} [topological_space α] {x : α} {U : topological_space.opens α} :
x U = (x U)

@[ext]
theorem topological_space.opens.ext {α : Type u_1} [topological_space α] {U V : topological_space.opens α} :
U = VU = V

@[ext]
theorem topological_space.opens.ext_iff {α : Type u_1} [topological_space α] {U V : topological_space.opens α} :
U = V U = V

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

Equations

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

Equations
@[instance]

Equations
@[simp]
theorem topological_space.opens.mk_inf_mk {α : Type u_1} [topological_space α] {U V : set α} {hU : is_open U} {hV : is_open V} :
U, hU⟩ V, hV⟩ = U V, _⟩

@[simp]
theorem topological_space.opens.coe_inf {α : Type u_1} [topological_space α] {U V : topological_space.opens α} :
(U V) = U V

@[simp]
theorem topological_space.opens.inter_eq {α : Type u_1} [topological_space α] (U V : topological_space.opens α) :
U V = U V

@[simp]
theorem topological_space.opens.union_eq {α : Type u_1} [topological_space α] (U V : topological_space.opens α) :
U V = U V

@[simp]
theorem topological_space.opens.empty_eq {α : Type u_1} [topological_space α] :

@[simp]
theorem topological_space.opens.Sup_s {α : Type u_1} [topological_space α] {Us : set (topological_space.opens α)} :
(Sup Us) = ⋃₀(coe '' Us)

theorem topological_space.opens.supr_def {α : Type u_1} [topological_space α] {ι : Sort u_2} (s : ι → topological_space.opens α) :
(⨆ (i : ι), s i) = ⋃ (i : ι), (s i), _⟩

@[simp]
theorem topological_space.opens.supr_mk {α : Type u_1} [topological_space α] {ι : 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} [topological_space α] {ι : Sort u_2} (s : ι → topological_space.opens α) :
(⨆ (i : ι), s i) = ⋃ (i : ι), (s i)

theorem topological_space.opens.mem_supr {α : Type u_1} [topological_space α] {ι : Sort u_2} {x : α} {s : ι → topological_space.opens α} :
x supr s ∃ (i : ι), x s i

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)

def topological_space.opens.comap {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :

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

Equations
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 β} :

@[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 β) :

@[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 β) :

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 γ) :

@[simp]

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

Equations
def topological_space.open_nhds_of {α : Type u_1} [topological_space α] :
α → Type u_1

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

Equations