# 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 α (CompleteLattice, Frame) and OpenNhdsOf 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

The type of open subsets of a topological space.

• carrier : Set α

The underlying set of a bundled TopologicalSpace.Opens object.

• is_open' : IsOpen self.carrier

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

Instances For
theorem TopologicalSpace.Opens.is_open' {α : Type u_2} [] (self : ) :
IsOpen self.carrier

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

instance TopologicalSpace.Opens.instSetLike {α : Type u_2} [] :
Equations
• TopologicalSpace.Opens.instSetLike = { coe := TopologicalSpace.Opens.carrier, coe_injective' := }
instance TopologicalSpace.Opens.instCanLiftSetCoeIsOpen {α : Type u_2} [] :
CanLift (Set α) SetLike.coe IsOpen
Equations
• =
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 U (U).Nonempty
theorem TopologicalSpace.Opens.nonempty_coe {α : Type u_2} [] {U : } :
(U).Nonempty ∃ (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' := } = U
def TopologicalSpace.Opens.Simps.coe {α : Type u_2} [] (U : ) :
Set α

See Note [custom simps projection].

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

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

Equations
• = { carrier := , is_open' := }
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.

Equations
• TopologicalSpace.Opens.gi = { choice := fun (s : Set α) (hs : ) => { carrier := s, is_open' := }, gc := , u_l_le := , choice_eq := }
Instances For
Equations
• One or more equations did not get rendered due to their size.
@[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' := }
@[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.mk_empty {α : Type u_2} [] :
{ carrier := , is_open' := } =
@[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.mk_univ {α : Type u_2} [] :
{ carrier := Set.univ, is_open' := } =
@[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) = iS, i
@[simp]
theorem TopologicalSpace.Opens.coe_finset_sup {ι : Type u_1} {α : Type u_2} [] (f : ) (s : ) :
(s.sup f) = s.sup (SetLike.coe f)
@[simp]
theorem TopologicalSpace.Opens.coe_finset_inf {ι : Type u_1} {α : Type u_2} [] (f : ) (s : ) :
(s.inf f) = s.inf (SetLike.coe f)
Equations
• TopologicalSpace.Opens.instInhabited = { default := }
Equations
• TopologicalSpace.Opens.instUniqueOfIsEmpty = { toInhabited := TopologicalSpace.Opens.instInhabited, uniq := }
Equations
• =
@[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' := }
@[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' := } = { carrier := ⋃ (i : ι), s i, is_open' := }
@[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 uUs, x u
instance TopologicalSpace.Opens.instFrame {α : Type u_2} [] :
Equations
• TopologicalSpace.Opens.instFrame = let __src := ;
theorem TopologicalSpace.Opens.openEmbedding' {α : Type u_2} [] (U : ) :
OpenEmbedding Subtype.val
theorem TopologicalSpace.Opens.openEmbedding_of_le {α : Type u_2} [] {U : } {V : } (i : U V) :
theorem TopologicalSpace.Opens.not_nonempty_iff_eq_bot {α : Type u_2} [] (U : ) :
¬(U).Nonempty U =
theorem TopologicalSpace.Opens.ne_bot_iff_nonempty {α : Type u_2} [] (U : ) :
U (U).Nonempty
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.

Equations
Instances For
theorem TopologicalSpace.Opens.isBasis_iff_nbhd {α : Type u_2} [] {B : } :
∀ {U : } {x : α}, x UU'B, x U' U' U
theorem TopologicalSpace.Opens.isBasis_iff_cover {α : Type u_2} [] {B : } :
∀ (U : ), UsB, 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 : Set ι), s.Finite U = is, (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.

Equations
• = { toFun := fun (s : ) => { carrier := f ⁻¹' s, is_open' := }, map_inf' := , map_top' := , map_sSup' := }
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 : α ≃ₜ β) :
f.opensCongr = (TopologicalSpace.Opens.comap f.symm.toContinuousMap)
def Homeomorph.opensCongr {α : Type u_2} {β : Type u_3} [] [] (f : α ≃ₜ β) :

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

Equations
Instances For
@[simp]
theorem Homeomorph.opensCongr_symm {α : Type u_2} {β : Type u_3} [] [] (f : α ≃ₜ β) :
f.opensCongr.symm = f.symm.opensCongr
instance TopologicalSpace.Opens.instFinite {α : Type u_2} [] [] :
Equations
• =
structure TopologicalSpace.OpenNhdsOf {α : Type u_2} [] (x : α) extends :
Type u_2

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

• carrier : Set α
• is_open' : IsOpen self.carrier
• mem' : x self.carrier

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

Instances For
theorem TopologicalSpace.OpenNhdsOf.mem' {α : Type u_2} [] {x : α} (self : ) :
x self.carrier

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

theorem TopologicalSpace.OpenNhdsOf.toOpens_injective {α : Type u_2} [] {x : α} :
Function.Injective TopologicalSpace.OpenNhdsOf.toOpens
instance TopologicalSpace.OpenNhdsOf.instSetLike {α : Type u_2} [] {x : α} :
Equations
• TopologicalSpace.OpenNhdsOf.instSetLike = { coe := fun (U : ) => U.toOpens, coe_injective' := }
instance TopologicalSpace.OpenNhdsOf.canLiftSet {α : Type u_2} [] {x : α} :
CanLift (Set α) SetLike.coe fun (s : Set α) => x s
Equations
• =
theorem TopologicalSpace.OpenNhdsOf.mem {α : Type u_2} [] {x : α} (U : ) :
x U
theorem TopologicalSpace.OpenNhdsOf.isOpen {α : Type u_2} [] {x : α} (U : ) :
IsOpen U
instance TopologicalSpace.OpenNhdsOf.instOrderTop {α : Type u_2} [] {x : α} :
Equations
• TopologicalSpace.OpenNhdsOf.instOrderTop =
instance TopologicalSpace.OpenNhdsOf.instInhabited {α : Type u_2} [] {x : α} :
Equations
• TopologicalSpace.OpenNhdsOf.instInhabited = { default := }
instance TopologicalSpace.OpenNhdsOf.instInf {α : Type u_2} [] {x : α} :
Equations
• TopologicalSpace.OpenNhdsOf.instInf = { inf := fun (U V : ) => { toOpens := U.toOpens V.toOpens, mem' := } }
instance TopologicalSpace.OpenNhdsOf.instSup {α : Type u_2} [] {x : α} :
Equations
• TopologicalSpace.OpenNhdsOf.instSup = { sup := fun (U V : ) => { toOpens := U.toOpens V.toOpens, mem' := } }
instance TopologicalSpace.OpenNhdsOf.instUniqueOfSubsingleton {α : Type u_2} [] {x : α} [] :
Equations
• TopologicalSpace.OpenNhdsOf.instUniqueOfSubsingleton = { toInhabited := TopologicalSpace.OpenNhdsOf.instInhabited, uniq := }
instance TopologicalSpace.OpenNhdsOf.instDistribLattice {α : Type u_2} [] {x : α} :
Equations
theorem TopologicalSpace.OpenNhdsOf.basis_nhds {α : Type u_2} [] {x : α} :
(nhds x).HasBasis (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.

Equations
• One or more equations did not get rendered due to their size.
Instances For