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) [TopologicalSpace α] : 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.

instance TopologicalSpace.Opens.instSetLikeOpens {α : Type u_2} [TopologicalSpace α] : SetLike (TopologicalSpace.Opens α) α

instance TopologicalSpace.Opens.instCanLiftSetOpensCoeInstSetLikeOpensIsOpen {α : Type u_2} [TopologicalSpace α] : CanLift (Set α) (TopologicalSpace.Opens α) SetLike.coe IsOpen

theorem TopologicalSpace.Opens.forall {α : Type u_2} [TopologicalSpace α] {p : TopologicalSpace.Opens α → Prop} : ((U : TopologicalSpace.Opens α) → p U) ↔ (U : Set α) → (hU : IsOpen U) → p { carrier := U, is_open' := hU }

@[simp]

theorem TopologicalSpace.Opens.carrier_eq_coe {α : Type u_2} [TopologicalSpace α] (U : TopologicalSpace.Opens α) : U.carrier = ↑U

@[simp]

theorem TopologicalSpace.Opens.coe_mk {α : Type u_2} [TopologicalSpace α] {U : Set α} {hU : IsOpen 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 TopologicalSpace.Opens.mem_mk {α : Type u_2} [TopologicalSpace α] {x : α} {U : Set α} {h : IsOpen U} : x ∈ { carrier := U, is_open' := h } ↔ x ∈ U

theorem TopologicalSpace.Opens.nonempty_coeSort {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} : Nonempty { x // x ∈ U } ↔ Set.Nonempty ↑U

theorem TopologicalSpace.Opens.nonempty_coe {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} : Set.Nonempty ↑U ↔ ∃ x, x ∈ U

theorem TopologicalSpace.Opens.ext {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} {V : TopologicalSpace.Opens α} (h : ↑U = ↑V) : U = V

theorem TopologicalSpace.Opens.coe_inj {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} {V : TopologicalSpace.Opens α} : ↑U = ↑V ↔ U = V

theorem TopologicalSpace.Opens.isOpen {α : Type u_2} [TopologicalSpace α] (U : TopologicalSpace.Opens α) : IsOpen ↑U

@[simp]

theorem TopologicalSpace.Opens.mk_coe {α : Type u_2} [TopologicalSpace α] (U : TopologicalSpace.Opens α) : { carrier := ↑U, is_open' := (_ : IsOpen ↑U) } = U

def TopologicalSpace.Opens.Simps.coe {α : Type u_2} [TopologicalSpace α] (U : TopologicalSpace.Opens α) : Set α

See Note [custom simps projection].

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

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

theorem TopologicalSpace.Opens.gc {α : Type u_2} [TopologicalSpace α] : GaloisConnection SetLike.coe TopologicalSpace.Opens.interior

def TopologicalSpace.Opens.gi {α : Type u_2} [TopologicalSpace α] : GaloisCoinsertion SetLike.coe TopologicalSpace.Opens.interior

The galois coinsertion between sets and opens.

instance TopologicalSpace.Opens.instCompleteLatticeOpens {α : Type u_2} [TopologicalSpace α] : CompleteLattice (TopologicalSpace.Opens α)

@[simp]

theorem TopologicalSpace.Opens.mk_inf_mk {α : Type u_2} [TopologicalSpace α] {U : Set α} {V : Set α} {hU : IsOpen U} {hV : IsOpen V} : { 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} [TopologicalSpace α] (s : TopologicalSpace.Opens α) (t : TopologicalSpace.Opens α) : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

theorem TopologicalSpace.Opens.coe_sup {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Opens α) (t : TopologicalSpace.Opens α) : ↑(s ⊔ t) = ↑s ∪ ↑t

@[simp]

theorem TopologicalSpace.Opens.coe_bot {α : Type u_2} [TopologicalSpace α] : ↑⊥ = ∅

@[simp]

theorem TopologicalSpace.Opens.coe_eq_empty {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} : ↑U = ∅ ↔ U = ⊥

@[simp]

theorem TopologicalSpace.Opens.coe_top {α : Type u_2} [TopologicalSpace α] : ↑⊤ = Set.univ

@[simp]

theorem TopologicalSpace.Opens.coe_eq_univ {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} : ↑U = Set.univ ↔ U = ⊤

@[simp]

theorem TopologicalSpace.Opens.coe_sSup {α : Type u_2} [TopologicalSpace α] {S : Set (TopologicalSpace.Opens α)} : ↑(sSup S) = ⋃ (i : TopologicalSpace.Opens α) (_ : i ∈ S), ↑i

@[simp]

theorem TopologicalSpace.Opens.coe_finset_sup {ι : Type u_1} {α : Type u_2} [TopologicalSpace α] (f : ι → TopologicalSpace.Opens α) (s : Finset ι) : ↑(Finset.sup s f) = Finset.sup s (SetLike.coe ∘ f)

@[simp]

theorem TopologicalSpace.Opens.coe_finset_inf {ι : Type u_1} {α : Type u_2} [TopologicalSpace α] (f : ι → TopologicalSpace.Opens α) (s : Finset ι) : ↑(Finset.inf s f) = Finset.inf s (SetLike.coe ∘ f)

instance TopologicalSpace.Opens.instInhabitedOpens {α : Type u_2} [TopologicalSpace α] : Inhabited (TopologicalSpace.Opens α)

instance TopologicalSpace.Opens.instUniqueOpens {α : Type u_2} [TopologicalSpace α] [IsEmpty α] : Unique (TopologicalSpace.Opens α)

instance TopologicalSpace.Opens.instNontrivialOpens {α : Type u_2} [TopologicalSpace α] [Nonempty α] : Nontrivial (TopologicalSpace.Opens α)

@[simp]

theorem TopologicalSpace.Opens.coe_iSup {α : Type u_2} [TopologicalSpace α] {ι : Sort u_5} (s : ι → TopologicalSpace.Opens α) : ↑(⨆ (i : ι), s i) = ⋃ (i : ι), ↑(s i)

theorem TopologicalSpace.Opens.iSup_def {α : Type u_2} [TopologicalSpace α] {ι : Sort u_5} (s : ι → TopologicalSpace.Opens α) : ⨆ (i : ι), s i = { carrier := ⋃ (i : ι), ↑(s i), is_open' := (_ : IsOpen (⋃ (i : ι), ↑(s i))) }

@[simp]

theorem TopologicalSpace.Opens.iSup_mk {α : Type u_2} [TopologicalSpace α] {ι : 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} [TopologicalSpace α] {ι : Sort u_5} {x : α} {s : ι → TopologicalSpace.Opens α} : x ∈ iSup s ↔ ∃ i, x ∈ s i

@[simp]

theorem TopologicalSpace.Opens.mem_sSup {α : Type u_2} [TopologicalSpace α] {Us : Set (TopologicalSpace.Opens α)} {x : α} : x ∈ sSup Us ↔ ∃ u, u ∈ Us ∧ x ∈ u

instance TopologicalSpace.Opens.instFrameOpens {α : Type u_2} [TopologicalSpace α] : Order.Frame (TopologicalSpace.Opens α)

theorem TopologicalSpace.Opens.openEmbedding_of_le {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} {V : TopologicalSpace.Opens α} (i : U ≤ V) : OpenEmbedding (Set.inclusion (_ : ↑U ⊆ ↑V))

theorem TopologicalSpace.Opens.not_nonempty_iff_eq_bot {α : Type u_2} [TopologicalSpace α] (U : TopologicalSpace.Opens α) : ¬Set.Nonempty ↑U ↔ U = ⊥

theorem TopologicalSpace.Opens.ne_bot_iff_nonempty {α : Type u_2} [TopologicalSpace α] (U : TopologicalSpace.Opens α) : U ≠ ⊥ ↔ Set.Nonempty ↑U

theorem TopologicalSpace.Opens.eq_bot_or_top {α : Type u_5} [t : TopologicalSpace α] (h : t = ⊤) (U : TopologicalSpace.Opens α) : U = ⊥ ∨ U = ⊤

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

instance TopologicalSpace.Opens.instIsSimpleOrderOpensToLEToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensToBoundedOrder {α : Type u_2} [TopologicalSpace α] [Nonempty α] [Subsingleton α] : IsSimpleOrder (TopologicalSpace.Opens α)

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

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

theorem TopologicalSpace.Opens.isBasis_iff_nbhd {α : Type u_2} [TopologicalSpace α] {B : Set (TopologicalSpace.Opens α)} : TopologicalSpace.Opens.IsBasis B ↔ ∀ {U : TopologicalSpace.Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U

theorem TopologicalSpace.Opens.isBasis_iff_cover {α : Type u_2} [TopologicalSpace α] {B : Set (TopologicalSpace.Opens α)} : TopologicalSpace.Opens.IsBasis B ↔ ∀ (U : TopologicalSpace.Opens α), ∃ Us, Us ⊆ B ∧ U = sSup Us

theorem TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion {α : Type u_2} [TopologicalSpace α] {ι : Type u_5} (b : ι → TopologicalSpace.Opens α) (hb : TopologicalSpace.Opens.IsBasis (Set.range b)) (hb' : ∀ (i : ι), IsCompact ↑(b i)) (U : Set α) : IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite 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} [TopologicalSpace α] (s : TopologicalSpace.Opens α) : CompleteLattice.IsCompactElement s ↔ IsCompact ↑s

def TopologicalSpace.Opens.comap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) : FrameHom (TopologicalSpace.Opens β) (TopologicalSpace.Opens α)

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

@[simp]

theorem TopologicalSpace.Opens.comap_id {α : Type u_2} [TopologicalSpace α] : TopologicalSpace.Opens.comap (ContinuousMap.id α) = FrameHom.id (TopologicalSpace.Opens α)

theorem TopologicalSpace.Opens.comap_mono {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) {s : TopologicalSpace.Opens β} {t : TopologicalSpace.Opens β} (h : s ≤ t) : ↑(TopologicalSpace.Opens.comap f) s ≤ ↑(TopologicalSpace.Opens.comap f) t

@[simp]

theorem TopologicalSpace.Opens.coe_comap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (U : TopologicalSpace.Opens β) : ↑(↑(TopologicalSpace.Opens.comap f) U) = ↑f ⁻¹' ↑U

theorem TopologicalSpace.Opens.comap_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (g : C(β, γ)) (f : C(α, β)) : TopologicalSpace.Opens.comap (ContinuousMap.comp g f) = FrameHom.comp (TopologicalSpace.Opens.comap f) (TopologicalSpace.Opens.comap g)

theorem TopologicalSpace.Opens.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (g : C(β, γ)) (f : C(α, β)) (U : TopologicalSpace.Opens γ) : ↑(TopologicalSpace.Opens.comap f) (↑(TopologicalSpace.Opens.comap g) U) = ↑(TopologicalSpace.Opens.comap (ContinuousMap.comp g f)) U

theorem TopologicalSpace.Opens.comap_injective {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [T0Space β] : Function.Injective TopologicalSpace.Opens.comap

@[simp]

theorem Homeomorph.opensCongr_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : ↑(Homeomorph.opensCongr f) = ↑(TopologicalSpace.Opens.comap (Homeomorph.toContinuousMap (Homeomorph.symm f)))

def Homeomorph.opensCongr {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : TopologicalSpace.Opens α ≃o TopologicalSpace.Opens β

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

@[simp]

theorem Homeomorph.opensCongr_symm {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : OrderIso.symm (Homeomorph.opensCongr f) = Homeomorph.opensCongr (Homeomorph.symm f)

instance TopologicalSpace.Opens.instFiniteOpens {α : Type u_2} [TopologicalSpace α] [Finite α] : Finite (TopologicalSpace.Opens α)

structure TopologicalSpace.OpenNhdsOf {α : Type u_2} [TopologicalSpace α] (x : α) extends TopologicalSpace.Opens : 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.

theorem TopologicalSpace.OpenNhdsOf.toOpens_injective {α : Type u_2} [TopologicalSpace α] {x : α} : Function.Injective TopologicalSpace.OpenNhdsOf.toOpens

instance TopologicalSpace.OpenNhdsOf.instSetLikeOpenNhdsOf {α : Type u_2} [TopologicalSpace α] {x : α} : SetLike (TopologicalSpace.OpenNhdsOf x) α

instance TopologicalSpace.OpenNhdsOf.canLiftSet {α : Type u_2} [TopologicalSpace α] {x : α} : CanLift (Set α) (TopologicalSpace.OpenNhdsOf x) SetLike.coe fun s => IsOpen s ∧ x ∈ s

theorem TopologicalSpace.OpenNhdsOf.mem {α : Type u_2} [TopologicalSpace α] {x : α} (U : TopologicalSpace.OpenNhdsOf x) : x ∈ U

theorem TopologicalSpace.OpenNhdsOf.isOpen {α : Type u_2} [TopologicalSpace α] {x : α} (U : TopologicalSpace.OpenNhdsOf x) : IsOpen ↑U

instance TopologicalSpace.OpenNhdsOf.instOrderTopOpenNhdsOfToLEToPreorderInstPartialOrderInstSetLikeOpenNhdsOf {α : Type u_2} [TopologicalSpace α] {x : α} : OrderTop (TopologicalSpace.OpenNhdsOf x)

instance TopologicalSpace.OpenNhdsOf.instInhabitedOpenNhdsOf {α : Type u_2} [TopologicalSpace α] {x : α} : Inhabited (TopologicalSpace.OpenNhdsOf x)

instance TopologicalSpace.OpenNhdsOf.instInfOpenNhdsOf {α : Type u_2} [TopologicalSpace α] {x : α} : Inf (TopologicalSpace.OpenNhdsOf x)

instance TopologicalSpace.OpenNhdsOf.instSupOpenNhdsOf {α : Type u_2} [TopologicalSpace α] {x : α} : Sup (TopologicalSpace.OpenNhdsOf x)

instance TopologicalSpace.OpenNhdsOf.instUniqueOpenNhdsOf {α : Type u_2} [TopologicalSpace α] {x : α} [Subsingleton α] : Unique (TopologicalSpace.OpenNhdsOf x)

instance TopologicalSpace.OpenNhdsOf.instDistribLatticeOpenNhdsOf {α : Type u_2} [TopologicalSpace α] {x : α} : DistribLattice (TopologicalSpace.OpenNhdsOf x)

theorem TopologicalSpace.OpenNhdsOf.basis_nhds {α : Type u_2} [TopologicalSpace α] {x : α} : Filter.HasBasis (nhds x) (fun x => True) SetLike.coe

def TopologicalSpace.OpenNhdsOf.comap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (x : α) : LatticeHom (TopologicalSpace.OpenNhdsOf (↑f x)) (TopologicalSpace.OpenNhdsOf x)

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