mathlib documentation

topology.sets.opens

Open sets #

Summary #

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

Main Definitions #

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

@[protected, instance]
Equations
@[simp]
@[simp]
theorem topological_space.opens.mem_coe {α : Type u_2} [topological_space α] {x : α} {U : topological_space.opens α} :
x U = (x U)
@[simp]
theorem topological_space.opens.mem_mk {α : Type u_2} [topological_space α] {x : α} {U : set α} {h : is_open U} :
x U, h⟩ x U
@[ext]
theorem topological_space.opens.ext {α : Type u_2} [topological_space α] {U V : topological_space.opens α} (h : U = V) :
U = V
@[ext]

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

Equations

The galois coinsertion between sets and opens.

Equations
@[protected, instance]
Equations
@[simp]
theorem topological_space.opens.mk_inf_mk {α : Type u_2} [topological_space α] {U V : set α} {hU : is_open U} {hV : is_open V} :
U, hU⟩ V, hV⟩ = U V, _⟩
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem topological_space.opens.coe_finset_sup {ι : Type u_1} {α : Type u_2} [topological_space α] (f : ι topological_space.opens α) (s : finset ι) :
(s.sup f) = s.sup (coe f)
@[simp, norm_cast]
theorem topological_space.opens.coe_finset_inf {ι : Type u_1} {α : Type u_2} [topological_space α] (f : ι topological_space.opens α) (s : finset ι) :
(s.inf f) = s.inf (coe f)
@[simp]
@[simp]
theorem topological_space.opens.supr_def {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι topological_space.opens α) :
( (i : ι), s i) = (i : ι), (s i), _⟩
@[simp]
theorem topological_space.opens.supr_mk {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι set α) (h : (i : ι), is_open (s i)) :
( (i : ι), s i, _⟩) = (i : ι), s i, _⟩
@[simp, norm_cast]
theorem topological_space.opens.coe_supr {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι topological_space.opens α) :
( (i : ι), s i) = (i : ι), (s i)
@[simp]
theorem topological_space.opens.mem_supr {α : Type u_2} [topological_space α] {ι : Sort u_1} {x : α} {s : ι topological_space.opens α} :
x supr s (i : ι), x s i
@[simp]
theorem topological_space.opens.mem_Sup {α : Type u_2} [topological_space α] {Us : set (topological_space.opens α)} {x : α} :
x has_Sup.Sup Us (u : topological_space.opens α) (H : u Us), x u
theorem topological_space.opens.eq_bot_or_top {α : Type u_1} [t : topological_space α] (h : t = ) (U : topological_space.opens α) :
U = U =

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
theorem topological_space.opens.is_compact_open_iff_eq_finite_Union_of_is_basis {α : Type u_2} [topological_space α] {ι : Type u_1} (b : ι topological_space.opens α) (hb : topological_space.opens.is_basis (set.range b)) (hb' : (i : ι), is_compact (b i)) (U : set α) :
is_compact U is_open U (s : set ι), s.finite U = (i : ι) (H : i s), (b i)

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
@[protected, simp]

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

Equations
@[protected, simp]

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

Equations
def topological_space.open_nhds_of {α : Type u_2} [topological_space α] (x : α) :
Type u_2

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

Equations
Instances for topological_space.open_nhds_of
@[protected, instance]