mathlib3 documentation

topology.sets.opens

Open sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Summary #

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

Main Definitions #

Bundled open sets #

Bundled open neighborhoods #

Main results #

We define order structures on both opens α (complete_structure, frame) and open_nhds_of x (order_top, distrib_lattice).

theorem topological_space.opens.forall {α : Type u_2} [topological_space α] {p : topological_space.opens α Prop} :
( (U : topological_space.opens α), p U) (U : set α) (hU : is_open U), p {carrier := U, is_open' := hU}
@[simp]
theorem topological_space.opens.coe_mk {α : Type u_2} [topological_space α] {U : set α} {hU : is_open U} :
{carrier := U, is_open' := hU} = U

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

@[simp]
theorem topological_space.opens.mem_mk {α : Type u_2} [topological_space α] {x : α} {U : set α} {h : is_open U} :
x {carrier := U, is_open' := h} x U
@[ext]
theorem topological_space.opens.ext {α : Type u_2} [topological_space α] {U V : topological_space.opens α} (h : U = V) :
U = V
@[simp]
@[simp]

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} :
{carrier := U, is_open' := hU} {carrier := V, is_open' := hV} = {carrier := U V, is_open' := _}
@[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)
theorem topological_space.opens.supr_def {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι topological_space.opens α) :
( (i : ι), s i) = {carrier := (i : ι), (s i), is_open' := _}
@[simp]
theorem topological_space.opens.supr_mk {α : Type u_2} [topological_space α] {ι : Sort u_1} (s : ι set α) (h : (i : ι), is_open (s i)) :
( (i : ι), {carrier := s i, is_open' := _}) = {carrier := (i : ι), s i, is_open' := _}
@[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_basis.is_compact_open_iff_eq_finite_Union {α : 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

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

Equations
@[simp]
theorem homeomorph.opens_congr_symm {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] (f : α ≃ₜ β) :
@[protected, instance]
@[protected]
@[protected, instance]
Equations

Preimage of an open neighborhood of f x under a continuous map f as a lattice_hom.

Equations