# Documentation

Mathlib.Topology.Sets.Opens

# Open sets #

## Summary #

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

## Main Definitions #

### Bundled open sets #

• TopologicalSpace.Opens α is the type of open subsets of a topological space α.
• TopologicalSpace.Opens.IsBasis is a predicate saying that a set of openss form a topological basis.
• TopologicalSpace.Opens.comap: preimage of an open set under a continuous map as a FrameHom.
• Homeomorph.opensCongr: order-preserving equivalence between open sets in the domain and the codomain of a homeomorphism.

### Bundled open neighborhoods #

• TopologicalSpace.OpenNhdsOf x is the type of open subsets of a topological space α containing x : α.
• TopologicalSpace.OpenNhdsOf.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 (OrderTop, DistribLattice).

## TODO #

• Rename TopologicalSpace.Opens to Open?
• Port the auto_cases tactic version (as a plugin if the ported auto_cases will allow plugins).
structure TopologicalSpace.Opens (α : Type u_2) [] :
Type u_2
• carrier : Set α

The underlying set of a bundled TopologicalSpace.Opens object.

• is_open' : IsOpen s.carrier

The TopologicalSpace.Opens.carrier _ is an open set.

The type of open subsets of a topological space.

Instances For
theorem TopologicalSpace.Opens.forall {α : Type u_2} [] {p : } :
((U : ) → p U) (U : Set α) → (hU : ) → p { carrier := U, is_open' := hU }
@[simp]
theorem TopologicalSpace.Opens.carrier_eq_coe {α : Type u_2} [] (U : ) :
U.carrier = U
@[simp]
theorem TopologicalSpace.Opens.coe_mk {α : Type u_2} [] {U : Set α} {hU : } :
{ carrier := U, is_open' := hU } = U

the coercion Opens α → Set α applied to a pair is the same as taking the first component

@[simp]
theorem TopologicalSpace.Opens.mem_mk {α : Type u_2} [] {x : α} {U : Set α} {h : } :
x { carrier := U, is_open' := h } x U
theorem TopologicalSpace.Opens.nonempty_coeSort {α : Type u_2} [] {U : } :
Nonempty { x // x U }
theorem TopologicalSpace.Opens.nonempty_coe {α : Type u_2} [] {U : } :
x, x U
theorem TopologicalSpace.Opens.ext {α : Type u_2} [] {U : } {V : } (h : U = V) :
U = V
theorem TopologicalSpace.Opens.coe_inj {α : Type u_2} [] {U : } {V : } :
U = V U = V
theorem TopologicalSpace.Opens.isOpen {α : Type u_2} [] (U : ) :
IsOpen U
@[simp]
theorem TopologicalSpace.Opens.mk_coe {α : Type u_2} [] (U : ) :
{ carrier := U, is_open' := (_ : IsOpen U) } = U
def TopologicalSpace.Opens.Simps.coe {α : Type u_2} [] (U : ) :
Set α

See Note [custom simps projection].

Instances For
def TopologicalSpace.Opens.interior {α : Type u_2} [] (s : Set α) :

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

Instances For
theorem TopologicalSpace.Opens.gc {α : Type u_2} [] :
GaloisConnection SetLike.coe TopologicalSpace.Opens.interior
def TopologicalSpace.Opens.gi {α : Type u_2} [] :
GaloisCoinsertion SetLike.coe TopologicalSpace.Opens.interior

The galois coinsertion between sets and opens.

Instances For
@[simp]
theorem TopologicalSpace.Opens.mk_inf_mk {α : Type u_2} [] {U : Set α} {V : Set α} {hU : } {hV : } :
{ carrier := U, is_open' := hU } { carrier := V, is_open' := hV } = { carrier := U V, is_open' := (_ : IsOpen (U V)) }
@[simp]
theorem TopologicalSpace.Opens.coe_inf {α : Type u_2} [] (s : ) (t : ) :
↑(s t) = s t
@[simp]
theorem TopologicalSpace.Opens.coe_sup {α : Type u_2} [] (s : ) (t : ) :
↑(s t) = s t
@[simp]
theorem TopologicalSpace.Opens.coe_bot {α : Type u_2} [] :
=
@[simp]
theorem TopologicalSpace.Opens.coe_eq_empty {α : Type u_2} [] {U : } :
U = U =
@[simp]
theorem TopologicalSpace.Opens.coe_top {α : Type u_2} [] :
= Set.univ
@[simp]
theorem TopologicalSpace.Opens.coe_eq_univ {α : Type u_2} [] {U : } :
U = Set.univ U =
@[simp]
theorem TopologicalSpace.Opens.coe_sSup {α : Type u_2} [] {S : } :
↑(sSup S) = ⋃ (i : ) (_ : i S), i
@[simp]
theorem TopologicalSpace.Opens.coe_finset_sup {ι : Type u_1} {α : Type u_2} [] (f : ) (s : ) :
↑() = Finset.sup s (SetLike.coe f)
@[simp]
theorem TopologicalSpace.Opens.coe_finset_inf {ι : Type u_1} {α : Type u_2} [] (f : ) (s : ) :
↑() = Finset.inf s (SetLike.coe f)
@[simp]
theorem TopologicalSpace.Opens.coe_iSup {α : Type u_2} [] {ι : Sort u_5} (s : ) :
↑(⨆ (i : ι), s i) = ⋃ (i : ι), ↑(s i)
theorem TopologicalSpace.Opens.iSup_def {α : Type u_2} [] {ι : Sort u_5} (s : ) :
⨆ (i : ι), s i = { carrier := ⋃ (i : ι), ↑(s i), is_open' := (_ : IsOpen (⋃ (i : ι), ↑(s i))) }
@[simp]
theorem TopologicalSpace.Opens.iSup_mk {α : Type u_2} [] {ι : Sort u_5} (s : ιSet α) (h : ∀ (i : ι), IsOpen (s i)) :
⨆ (i : ι), { carrier := s i, is_open' := h i } = { carrier := ⋃ (i : ι), s i, is_open' := (_ : IsOpen (⋃ (i : ι), s i)) }
@[simp]
theorem TopologicalSpace.Opens.mem_iSup {α : Type u_2} [] {ι : Sort u_5} {x : α} {s : } :
x iSup s i, x s i
@[simp]
theorem TopologicalSpace.Opens.mem_sSup {α : Type u_2} [] {Us : } {x : α} :
x sSup Us u, u Us x u
theorem TopologicalSpace.Opens.openEmbedding_of_le {α : Type u_2} [] {U : } {V : } (i : U V) :
OpenEmbedding (Set.inclusion (_ : U V))
theorem TopologicalSpace.Opens.eq_bot_or_top {α : Type u_5} [t : ] (h : t = ) (U : ) :
U = U =

An open set in the indiscrete topology is either empty or the whole space.

def TopologicalSpace.Opens.IsBasis {α : Type u_2} [] (B : ) :

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

Instances For
theorem TopologicalSpace.Opens.isBasis_iff_nbhd {α : Type u_2} [] {B : } :
∀ {U : } {x : α}, x UU', U' B x U' U' U
theorem TopologicalSpace.Opens.isBasis_iff_cover {α : Type u_2} [] {B : } :
∀ (U : ), Us, Us B U = sSup Us
theorem TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion {α : Type u_2} [] {ι : Type u_5} (b : ) (hb : ) (hb' : ∀ (i : ι), IsCompact ↑(b i)) (U : Set α) :
s, U = ⋃ (i : ι) (_ : 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

@[simp]
theorem TopologicalSpace.Opens.isCompactElement_iff {α : Type u_2} [] (s : ) :
def TopologicalSpace.Opens.comap {α : Type u_2} {β : Type u_3} [] [] (f : C(α, β)) :

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

Instances For
@[simp]
theorem TopologicalSpace.Opens.comap_id {α : Type u_2} [] :
theorem TopologicalSpace.Opens.comap_mono {α : Type u_2} {β : Type u_3} [] [] (f : C(α, β)) {s : } {t : } (h : s t) :
@[simp]
theorem TopologicalSpace.Opens.coe_comap {α : Type u_2} {β : Type u_3} [] [] (f : C(α, β)) (U : ) :
↑() = f ⁻¹' U
theorem TopologicalSpace.Opens.comap_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (g : C(β, γ)) (f : C(α, β)) :
theorem TopologicalSpace.Opens.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] (g : C(β, γ)) (f : C(α, β)) (U : ) :
↑() () =
theorem TopologicalSpace.Opens.comap_injective {α : Type u_2} {β : Type u_3} [] [] [] :
Function.Injective TopologicalSpace.Opens.comap
@[simp]
theorem Homeomorph.opensCongr_apply {α : Type u_2} {β : Type u_3} [] [] (f : α ≃ₜ β) :
def Homeomorph.opensCongr {α : Type u_2} {β : Type u_3} [] [] (f : α ≃ₜ β) :

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

Instances For
@[simp]
theorem Homeomorph.opensCongr_symm {α : Type u_2} {β : Type u_3} [] [] (f : α ≃ₜ β) :
structure TopologicalSpace.OpenNhdsOf {α : Type u_2} [] (x : α) extends :
Type u_2
• carrier : Set α
• is_open' : IsOpen s.carrier
• mem' : x s.carrier

The point x belongs to every U : TopologicalSpace.OpenNhdsOf x.

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

Instances For
theorem TopologicalSpace.OpenNhdsOf.toOpens_injective {α : Type u_2} [] {x : α} :
Function.Injective TopologicalSpace.OpenNhdsOf.toOpens
instance TopologicalSpace.OpenNhdsOf.canLiftSet {α : Type u_2} [] {x : α} :
CanLift (Set α) () SetLike.coe fun s => x s
theorem TopologicalSpace.OpenNhdsOf.mem {α : Type u_2} [] {x : α} (U : ) :
x U
theorem TopologicalSpace.OpenNhdsOf.isOpen {α : Type u_2} [] {x : α} (U : ) :
IsOpen U
theorem TopologicalSpace.OpenNhdsOf.basis_nhds {α : Type u_2} [] {x : α} :
Filter.HasBasis (nhds x) (fun x => True) SetLike.coe
def TopologicalSpace.OpenNhdsOf.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 LatticeHom.

Instances For