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

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

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

instance TopologicalSpace.Opens.instSecondCountableOpens {α : Type u_2} [TopologicalSpace α] [SecondCountableTopology α] (U : Opens α) : SecondCountableTopology ↥U

theorem TopologicalSpace.Opens.forall {α : Type u_2} [TopologicalSpace α] {p : Opens α → Prop} : (∀ (U : 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 : 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 : Opens α} : Nonempty ↥U ↔ (↑U).Nonempty

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

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

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

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

@[reducible, inline]

abbrev TopologicalSpace.Opens.inclusion {α : Type u_2} [TopologicalSpace α] {U V : Opens α} (h : U ≤ V) : ↥U → ↥V

A version of Set.inclusion not requiring definitional abuse

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

@[simp]

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

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

See Note [custom simps projection].

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

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

@[simp]

theorem TopologicalSpace.Opens.coe_interior {α : Type u_2} [TopologicalSpace α] (s : Set α) : ↑(Opens.interior s) = interior s

@[simp]

theorem TopologicalSpace.Opens.mem_interior {α : Type u_2} [TopologicalSpace α] {s : Set α} {x : α} : x ∈ Opens.interior s ↔ x ∈ interior s

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

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

The galois coinsertion between sets and opens.

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

@[simp]

theorem TopologicalSpace.Opens.mk_inf_mk {α : Type u_2} [TopologicalSpace α] {U V : Set α} {hU : IsOpen U} {hV : IsOpen V} : { carrier := U, is_open' := hU } ⊓ { carrier := V, is_open' := hV } = { carrier := U ⊓ V, is_open' := ⋯ }

@[simp]

theorem TopologicalSpace.Opens.coe_inf {α : Type u_2} [TopologicalSpace α] (s t : Opens α) : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

theorem TopologicalSpace.Opens.mem_inf {α : Type u_2} [TopologicalSpace α] {s t : Opens α} {x : α} : x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t

@[simp]

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

@[simp]

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

@[simp]

theorem TopologicalSpace.Opens.mem_bot {α : Type u_2} [TopologicalSpace α] {x : α} : x ∈ ⊥ ↔ False

@[simp]

theorem TopologicalSpace.Opens.mk_empty {α : Type u_2} [TopologicalSpace α] : { carrier := ∅, is_open' := ⋯ } = ⊥

@[simp]

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

@[simp]

theorem TopologicalSpace.Opens.mem_top {α : Type u_2} [TopologicalSpace α] (x : α) : x ∈ ⊤

@[simp]

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

@[simp]

theorem TopologicalSpace.Opens.mk_univ {α : Type u_2} [TopologicalSpace α] : { carrier := Set.univ, is_open' := ⋯ } = ⊤

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

@[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' := ⋯ } = { carrier := ⋃ (i : ι), s i, is_open' := ⋯ }

@[simp]

theorem TopologicalSpace.Opens.mem_iSup {α : Type u_2} [TopologicalSpace α] {ι : Sort u_5} {x : α} {s : ι → Opens α} : x ∈ iSup s ↔ ∃ (i : ι), x ∈ s i

@[simp]

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

def TopologicalSpace.Opens.frameMinimalAxioms {α : Type u_2} [TopologicalSpace α] : Order.Frame.MinimalAxioms (Opens α)

Open sets in a topological space form a frame.

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

theorem TopologicalSpace.Opens.isOpenEmbedding' {α : Type u_2} [TopologicalSpace α] (U : Opens α) : Topology.IsOpenEmbedding Subtype.val

theorem TopologicalSpace.Opens.isOpenEmbedding_of_le {α : Type u_2} [TopologicalSpace α] {U V : Opens α} (i : U ≤ V) : Topology.IsOpenEmbedding (Set.inclusion ⋯)

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

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

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

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

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

def TopologicalSpace.Opens.IsBasis {α : Type u_2} [TopologicalSpace α] (B : Set (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 (Opens α)} : IsBasis B ↔ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

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

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

theorem TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact {α : Type u_2} [TopologicalSpace α] {B : Set (Opens α)} (hB : IsBasis B) {U : Opens α} (hU : IsCompact U.carrier) : ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us

theorem TopologicalSpace.Opens.IsBasis.le_iff {α : Type u_5} {t₁ t₂ : TopologicalSpace α} {Us : Set (Opens α)} (hUs : IsBasis Us) : t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen ↑U

theorem TopologicalSpace.Opens.isBasis_sigma {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] {B : (i : ι) → Set (Opens (α i))} (hB : ∀ (i : ι), IsBasis (B i)) : IsBasis (⋃ (i : ι), (fun (U : Opens (α i)) => { carrier := Sigma.mk i '' U.carrier, is_open' := ⋯ }) '' B i)

theorem TopologicalSpace.Opens.IsBasis.of_isInducing {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {B : Set (Opens β)} (H : IsBasis B) {f : α → β} (h : Topology.IsInducing f) : IsBasis {x : Opens α | ∃ U ∈ B, { carrier := f ⁻¹' ↑U, is_open' := ⋯ } = x}

@[simp]

theorem TopologicalSpace.Opens.isCompactElement_iff {α : Type u_2} [TopologicalSpace α] (s : Opens α) : CompleteLattice.IsCompactElement s ↔ IsCompact ↑s

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

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem TopologicalSpace.Opens.mem_comap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : C(α, β)} {U : Opens β} {x : α} : x ∈ (comap f) U ↔ f x ∈ U

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

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

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

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_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : ⇑f.opensCongr = ⇑(TopologicalSpace.Opens.comap ↑f.symm)

@[simp]

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

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

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

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

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

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

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

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

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

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

instance TopologicalSpace.OpenNhdsOf.instMin {α : Type u_2} [TopologicalSpace α] {x : α} : Min (OpenNhdsOf x)

instance TopologicalSpace.OpenNhdsOf.instMax {α : Type u_2} [TopologicalSpace α] {x : α} : Max (OpenNhdsOf x)

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

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

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

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

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