# mathlib3documentation

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 #

• opens α is the type of open subsets of a topological space α.
• opens.is_basis is a predicate saying that a set of openss form a topological basis.
• opens.comap: preimage of an open set under a continuous map as a frame_hom.
• homeomorph.opens_congr: order-preserving equivalence between open sets in the domain and the codomain of a homeomorphism.

### Bundled open neighborhoods #

• open_nhds_of x is the type of open subsets of a topological space α containing x : α.
• open_nhds_of.comap f x U is the preimage of open neighborhood U of f x under f : C(α, β).

## Main results #

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

structure topological_space.opens (α : Type u_2)  :
Type u_2

The type of open subsets of a topological space.

Instances for topological_space.opens
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem topological_space.opens.forall {α : Type u_2} {p : Prop} :
( (U : , p U) (U : set α) (hU : is_open U), p {carrier := U, is_open' := hU}
@[simp]
theorem topological_space.opens.coe_mk {α : Type u_2} {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} {x : α} {U : set α} {h : is_open U} :
x {carrier := U, is_open' := h} x U
@[protected, simp]
@[ext]
theorem topological_space.opens.ext {α : Type u_2} {U V : topological_space.opens α} (h : U = V) :
U = V
@[simp]
theorem topological_space.opens.coe_inj {α : Type u_2} {U V : topological_space.opens α} :
U = V U = V
@[protected]
@[simp]
theorem topological_space.opens.mk_coe {α : Type u_2} (U : topological_space.opens α) :
{carrier := U, is_open' := _} = U
Equations
def topological_space.opens.interior {α : Type u_2} (s : set α) :

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} {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]
theorem topological_space.opens.coe_inf {α : Type u_2} (s t : topological_space.opens α) :
(s t) = s t
@[simp, norm_cast]
theorem topological_space.opens.coe_sup {α : Type u_2} (s t : topological_space.opens α) :
(s t) = s t
@[simp, norm_cast]
theorem topological_space.opens.coe_bot {α : Type u_2}  :
@[simp, norm_cast]
theorem topological_space.opens.coe_top {α : Type u_2}  :
@[simp, norm_cast]
theorem topological_space.opens.coe_Sup {α : Type u_2} {S : set } :
(has_Sup.Sup S) = (i : (H : i S), i
@[simp, norm_cast]
theorem topological_space.opens.coe_finset_sup {ι : Type u_1} {α : Type u_2} (f : ι ) (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} (f : ι ) (s : finset ι) :
(s.inf f) = s.inf (coe f)
@[protected, instance]
Equations
theorem topological_space.opens.supr_def {α : Type u_2} {ι : Sort u_1} (s : ι ) :
( (i : ι), s i) = {carrier := (i : ι), (s i), is_open' := _}
@[simp]
theorem topological_space.opens.supr_mk {α : Type u_2} {ι : 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} {ι : Sort u_1} (s : ι ) :
( (i : ι), s i) = (i : ι), (s i)
@[simp]
theorem topological_space.opens.mem_supr {α : Type u_2} {ι : Sort u_1} {x : α} {s : ι } :
x supr s (i : ι), x s i
@[simp]
theorem topological_space.opens.mem_Sup {α : Type u_2} {Us : set } {x : α} :
x (u : (H : u Us), x u
@[protected, instance]
Equations
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.

def topological_space.opens.is_basis {α : Type u_2} (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_2} {B : set } :
{U : {x : α}, x U ( (U' : (H : U' B), x U' U' U)
theorem topological_space.opens.is_basis_iff_cover {α : Type u_2} {B : set } :
(U : , (Us : (H : Us B), U =
theorem topological_space.opens.is_basis.is_compact_open_iff_eq_finite_Union {α : Type u_2} {ι : Type u_1} (b : ι ) (hb' : (i : ι), is_compact (b i)) (U : set α) :
(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

def topological_space.opens.comap {α : Type u_2} {β : Type u_3} (f : C(α, β)) :

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

Equations
@[simp]
theorem topological_space.opens.comap_id {α : Type u_2}  :
theorem topological_space.opens.comap_mono {α : Type u_2} {β : Type u_3} (f : C(α, β)) {s t : topological_space.opens β} (h : s t) :
@[simp]
theorem topological_space.opens.coe_comap {α : Type u_2} {β : Type u_3} (f : C(α, β)) (U : topological_space.opens β) :
@[protected]
theorem topological_space.opens.comap_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : C(β, γ)) (f : C(α, β)) :
@[protected]
theorem topological_space.opens.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : C(β, γ)) (f : C(α, β)) (U : topological_space.opens γ) :
= U
theorem topological_space.opens.comap_injective {α : Type u_2} {β : Type u_3} [t0_space β] :
@[simp]
theorem homeomorph.opens_congr_apply {α : Type u_2} {β : Type u_3} (f : α ≃ₜ β) :
def homeomorph.opens_congr {α : Type u_2} {β : Type u_3} (f : α ≃ₜ β) :

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} (f : α ≃ₜ β) :
@[protected, instance]
def topological_space.opens.finite {α : Type u_2} [finite α] :
structure topological_space.open_nhds_of {α : Type u_2} (x : α) :
Type u_2

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

Instances for topological_space.open_nhds_of
@[protected, instance]
def topological_space.open_nhds_of.set_like {α : Type u_2} {x : α} :
Equations
@[protected, instance]
def topological_space.open_nhds_of.can_lift_set {α : Type u_2} {x : α} :
(λ (s : set α), x s)
Equations
@[protected]
theorem topological_space.open_nhds_of.mem {α : Type u_2} {x : α}  :
x U
@[protected]
theorem topological_space.open_nhds_of.is_open {α : Type u_2} {x : α}  :
@[protected, instance]
def topological_space.open_nhds_of.order_top {α : Type u_2} {x : α} :
Equations
@[protected, instance]
def topological_space.open_nhds_of.inhabited {α : Type u_2} {x : α} :
Equations
@[protected, instance]
def topological_space.open_nhds_of.has_inf {α : Type u_2} {x : α} :
Equations
@[protected, instance]
def topological_space.open_nhds_of.has_sup {α : Type u_2} {x : α} :
Equations
@[protected, instance]
Equations
theorem topological_space.open_nhds_of.basis_nhds {α : Type u_2} {x : α} :
(nhds x).has_basis (λ (U : , true) coe
def topological_space.open_nhds_of.comap {α : Type u_2} {β : Type u_3} (f : C(α, β)) (x : α) :

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

Equations

Find an auto_cases_tac which matches topological_space.opens.

A version of tactic.auto_cases that works for topological_space.opens.