Closed sets #

We define a few types of closed sets in a topological space.

Main Definitions #

For a topological space α,

TopologicalSpace.Closeds α: The type of closed sets.
TopologicalSpace.Clopens α: The type of clopen sets.

Closed sets #

source

structure TopologicalSpace.Closeds (α : Type u_4) [TopologicalSpace α] :

Type u_4

carrier : Set α
closed' : IsClosed s.carrier

The type of closed subsets of a topological space.

Instances For

source

instance TopologicalSpace.Closeds.instSetLikeCloseds {α : Type u_2} [TopologicalSpace α] :

SetLike (TopologicalSpace.Closeds α) α

source

instance TopologicalSpace.Closeds.instCanLiftSetClosedsCoeInstSetLikeClosedsIsClosed {α : Type u_2} [TopologicalSpace α] :

CanLift (Set α) (TopologicalSpace.Closeds α) SetLike.coe IsClosed

source

theorem TopologicalSpace.Closeds.closed {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Closeds α) :

IsClosed ↑s

source

def TopologicalSpace.Closeds.Simps.coe {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Closeds α) :

Set α

See Note [custom simps projection].

Instances For

source

theorem TopologicalSpace.Closeds.ext {α : Type u_2} [TopologicalSpace α] {s : TopologicalSpace.Closeds α} {t : TopologicalSpace.Closeds α} (h : ↑s = ↑t) :

s = t

source

@[simp]

theorem TopologicalSpace.Closeds.coe_mk {α : Type u_2} [TopologicalSpace α] (s : Set α) (h : IsClosed s) :

↑{ carrier := s, closed' := h } = s

source

def TopologicalSpace.Closeds.closure {α : Type u_2} [TopologicalSpace α] (s : Set α) :

TopologicalSpace.Closeds α

The closure of a set, as an element of TopologicalSpace.Closeds.

Instances For

source

theorem TopologicalSpace.Closeds.gc {α : Type u_2} [TopologicalSpace α] :

GaloisConnection TopologicalSpace.Closeds.closure SetLike.coe

source

def TopologicalSpace.Closeds.gi {α : Type u_2} [TopologicalSpace α] :

GaloisInsertion TopologicalSpace.Closeds.closure SetLike.coe

The galois coinsertion between sets and opens.

Instances For

source

instance TopologicalSpace.Closeds.instCompleteLatticeCloseds {α : Type u_2} [TopologicalSpace α] :

CompleteLattice (TopologicalSpace.Closeds α)

source

instance TopologicalSpace.Closeds.instInhabitedCloseds {α : Type u_2} [TopologicalSpace α] :

Inhabited (TopologicalSpace.Closeds α)

The type of closed sets is inhabited, with default element the empty set.

source

@[simp]

theorem TopologicalSpace.Closeds.coe_sup {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Closeds α) (t : TopologicalSpace.Closeds α) :

↑(s ⊔ t) = ↑s ∪ ↑t

source

@[simp]

theorem TopologicalSpace.Closeds.coe_inf {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Closeds α) (t : TopologicalSpace.Closeds α) :

↑(s ⊓ t) = ↑s ∩ ↑t

source

@[simp]

theorem TopologicalSpace.Closeds.coe_top {α : Type u_2} [TopologicalSpace α] :

↑⊤ = Set.univ

source

@[simp]

theorem TopologicalSpace.Closeds.coe_eq_univ {α : Type u_2} [TopologicalSpace α] {s : TopologicalSpace.Closeds α} :

↑s = Set.univ ↔ s = ⊤

source

@[simp]

theorem TopologicalSpace.Closeds.coe_bot {α : Type u_2} [TopologicalSpace α] :

↑⊥ = ∅

source

@[simp]

theorem TopologicalSpace.Closeds.coe_eq_empty {α : Type u_2} [TopologicalSpace α] {s : TopologicalSpace.Closeds α} :

↑s = ∅ ↔ s = ⊥

source

theorem TopologicalSpace.Closeds.coe_nonempty {α : Type u_2} [TopologicalSpace α] {s : TopologicalSpace.Closeds α} :

Set.Nonempty ↑s ↔ s ≠ ⊥

source

@[simp]

theorem TopologicalSpace.Closeds.coe_sInf {α : Type u_2} [TopologicalSpace α] {S : Set (TopologicalSpace.Closeds α)} :

↑(sInf S) = ⋂ (i : TopologicalSpace.Closeds α) (_ : i ∈ S), ↑i

source

@[simp]

theorem TopologicalSpace.Closeds.coe_finset_sup {ι : Type u_1} {α : Type u_2} [TopologicalSpace α] (f : ι → TopologicalSpace.Closeds α) (s : Finset ι) :

↑(Finset.sup s f) = Finset.sup s (SetLike.coe ∘ f)

source

@[simp]

theorem TopologicalSpace.Closeds.coe_finset_inf {ι : Type u_1} {α : Type u_2} [TopologicalSpace α] (f : ι → TopologicalSpace.Closeds α) (s : Finset ι) :

↑(Finset.inf s f) = Finset.inf s (SetLike.coe ∘ f)

source

@[simp]

theorem TopologicalSpace.Closeds.mem_sInf {α : Type u_2} [TopologicalSpace α] {S : Set (TopologicalSpace.Closeds α)} {x : α} :

x ∈ sInf S ↔ ∀ (s : TopologicalSpace.Closeds α), s ∈ S → x ∈ s

source

@[simp]

theorem TopologicalSpace.Closeds.mem_iInf {α : Type u_2} [TopologicalSpace α] {ι : Sort u_4} {x : α} {s : ι → TopologicalSpace.Closeds α} :

x ∈ iInf s ↔ ∀ (i : ι), x ∈ s i

source

@[simp]

theorem TopologicalSpace.Closeds.coe_iInf {α : Type u_2} [TopologicalSpace α] {ι : Sort u_4} (s : ι → TopologicalSpace.Closeds α) :

↑(⨅ (i : ι), s i) = ⋂ (i : ι), ↑(s i)

source

theorem TopologicalSpace.Closeds.iInf_def {α : Type u_2} [TopologicalSpace α] {ι : Sort u_4} (s : ι → TopologicalSpace.Closeds α) :

⨅ (i : ι), s i = { carrier := ⋂ (i : ι), ↑(s i), closed' := (_ : IsClosed (⋂ (i : ι), ↑(s i))) }

source

@[simp]

theorem TopologicalSpace.Closeds.iInf_mk {α : Type u_2} [TopologicalSpace α] {ι : Sort u_4} (s : ι → Set α) (h : ∀ (i : ι), IsClosed (s i)) :

⨅ (i : ι), { carrier := s i, closed' := h i } = { carrier := ⋂ (i : ι), s i, closed' := (_ : IsClosed (⋂ (i : ι), s i)) }

source

instance TopologicalSpace.Closeds.instCoframeCloseds {α : Type u_2} [TopologicalSpace α] :

Order.Coframe (TopologicalSpace.Closeds α)

source

@[simp]

theorem TopologicalSpace.Closeds.singleton_coe {α : Type u_2} [TopologicalSpace α] [T1Space α] (x : α) :

↑(TopologicalSpace.Closeds.singleton x) = {x}

source

def TopologicalSpace.Closeds.singleton {α : Type u_2} [TopologicalSpace α] [T1Space α] (x : α) :

TopologicalSpace.Closeds α

The term of TopologicalSpace.Closeds α corresponding to a singleton.

Instances For

source

@[simp]

theorem TopologicalSpace.Closeds.compl_coe {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Closeds α) :

↑(TopologicalSpace.Closeds.compl s) = (↑s)ᶜ

source

def TopologicalSpace.Closeds.compl {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Closeds α) :

TopologicalSpace.Opens α

The complement of a closed set as an open set.

Instances For

source

@[simp]

theorem TopologicalSpace.Opens.compl_coe {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Opens α) :

↑(TopologicalSpace.Opens.compl s) = (↑s)ᶜ

source

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

TopologicalSpace.Closeds α

The complement of an open set as a closed set.

Instances For

source

theorem TopologicalSpace.Closeds.compl_compl {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Closeds α) :

TopologicalSpace.Opens.compl (TopologicalSpace.Closeds.compl s) = s

source

theorem TopologicalSpace.Opens.compl_compl {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Opens α) :

TopologicalSpace.Closeds.compl (TopologicalSpace.Opens.compl s) = s

source

theorem TopologicalSpace.Closeds.compl_bijective {α : Type u_2} [TopologicalSpace α] :

Function.Bijective TopologicalSpace.Closeds.compl

source

theorem TopologicalSpace.Opens.compl_bijective {α : Type u_2} [TopologicalSpace α] :

Function.Bijective TopologicalSpace.Opens.compl

source

@[simp]

theorem TopologicalSpace.Closeds.complOrderIso_symm_apply (α : Type u_2) [TopologicalSpace α] :

∀ (a : (TopologicalSpace.Opens α)ᵒᵈ), ↑(RelIso.symm (TopologicalSpace.Closeds.complOrderIso α)) a = (TopologicalSpace.Opens.compl ∘ ↑OrderDual.ofDual) a

source

@[simp]

theorem TopologicalSpace.Closeds.complOrderIso_apply (α : Type u_2) [TopologicalSpace α] :

∀ (a : TopologicalSpace.Closeds α), ↑(TopologicalSpace.Closeds.complOrderIso α) a = (↑OrderDual.toDual ∘ TopologicalSpace.Closeds.compl) a

source

def TopologicalSpace.Closeds.complOrderIso (α : Type u_2) [TopologicalSpace α] :

TopologicalSpace.Closeds α ≃o (TopologicalSpace.Opens α)ᵒᵈ

TopologicalSpace.Closeds.compl as an OrderIso to the order dual of TopologicalSpace.Opens α.

Instances For

source

@[simp]

theorem TopologicalSpace.Opens.complOrderIso_symm_apply (α : Type u_2) [TopologicalSpace α] :

∀ (a : (TopologicalSpace.Closeds α)ᵒᵈ), ↑(RelIso.symm (TopologicalSpace.Opens.complOrderIso α)) a = (TopologicalSpace.Closeds.compl ∘ ↑OrderDual.ofDual) a

source

@[simp]

theorem TopologicalSpace.Opens.complOrderIso_apply (α : Type u_2) [TopologicalSpace α] :

∀ (a : TopologicalSpace.Opens α), ↑(TopologicalSpace.Opens.complOrderIso α) a = (↑OrderDual.toDual ∘ TopologicalSpace.Opens.compl) a

source

def TopologicalSpace.Opens.complOrderIso (α : Type u_2) [TopologicalSpace α] :

TopologicalSpace.Opens α ≃o (TopologicalSpace.Closeds α)ᵒᵈ

TopologicalSpace.Opens.compl as an OrderIso to the order dual of TopologicalSpace.Closeds α.

Instances For

source

theorem TopologicalSpace.Closeds.isAtom_iff {α : Type u_2} [TopologicalSpace α] [T1Space α] {s : TopologicalSpace.Closeds α} :

IsAtom s ↔ ∃ x, s = TopologicalSpace.Closeds.singleton x

in a T1Space, atoms of TopologicalSpace.Closeds α are precisely the TopologicalSpace.Closeds.singletons.

TODO: use minimal_nonempty_closed_eq_singleton to show that an atom in TopologicalSpace.Closeds in a T₀ space is a singleton.

source

theorem TopologicalSpace.Opens.isCoatom_iff {α : Type u_2} [TopologicalSpace α] [T1Space α] {s : TopologicalSpace.Opens α} :

IsCoatom s ↔ ∃ x, s = TopologicalSpace.Closeds.compl (TopologicalSpace.Closeds.singleton x)

in a T1Space, coatoms of TopologicalSpace.Opens α are precisely complements of singletons: (TopologicalSpace.Closeds.singleton x).compl.

Clopen sets #

source

structure TopologicalSpace.Clopens (α : Type u_4) [TopologicalSpace α] :

Type u_4

carrier : Set α
clopen' : IsClopen s.carrier

The type of clopen sets of a topological space.

Instances For

source

instance TopologicalSpace.Clopens.instSetLikeClopens {α : Type u_2} [TopologicalSpace α] :

SetLike (TopologicalSpace.Clopens α) α

source

theorem TopologicalSpace.Clopens.clopen {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Clopens α) :

IsClopen ↑s

source

def TopologicalSpace.Clopens.Simps.coe {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Clopens α) :

Set α

See Note [custom simps projection].

Instances For

source

@[simp]

theorem TopologicalSpace.Clopens.toOpens_coe {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Clopens α) :

↑(TopologicalSpace.Clopens.toOpens s) = ↑s

source

def TopologicalSpace.Clopens.toOpens {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Clopens α) :

TopologicalSpace.Opens α

Reinterpret a clopen as an open.

Instances For

source

theorem TopologicalSpace.Clopens.ext {α : Type u_2} [TopologicalSpace α] {s : TopologicalSpace.Clopens α} {t : TopologicalSpace.Clopens α} (h : ↑s = ↑t) :

s = t

source

@[simp]

theorem TopologicalSpace.Clopens.coe_mk {α : Type u_2} [TopologicalSpace α] (s : Set α) (h : IsClopen s) :

↑{ carrier := s, clopen' := h } = s

source

instance TopologicalSpace.Clopens.instSupClopens {α : Type u_2} [TopologicalSpace α] :

Sup (TopologicalSpace.Clopens α)

source

instance TopologicalSpace.Clopens.instInfClopens {α : Type u_2} [TopologicalSpace α] :

Inf (TopologicalSpace.Clopens α)

source

instance TopologicalSpace.Clopens.instTopClopens {α : Type u_2} [TopologicalSpace α] :

Top (TopologicalSpace.Clopens α)

source

instance TopologicalSpace.Clopens.instBotClopens {α : Type u_2} [TopologicalSpace α] :

Bot (TopologicalSpace.Clopens α)

source

instance TopologicalSpace.Clopens.instSDiffClopens {α : Type u_2} [TopologicalSpace α] :

SDiff (TopologicalSpace.Clopens α)

source

instance TopologicalSpace.Clopens.instHasComplClopens {α : Type u_2} [TopologicalSpace α] :

HasCompl (TopologicalSpace.Clopens α)

source

instance TopologicalSpace.Clopens.instBooleanAlgebraClopens {α : Type u_2} [TopologicalSpace α] :

BooleanAlgebra (TopologicalSpace.Clopens α)

source

@[simp]

theorem TopologicalSpace.Clopens.coe_sup {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Clopens α) (t : TopologicalSpace.Clopens α) :

↑(s ⊔ t) = ↑s ∪ ↑t

source

@[simp]

theorem TopologicalSpace.Clopens.coe_inf {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Clopens α) (t : TopologicalSpace.Clopens α) :

↑(s ⊓ t) = ↑s ∩ ↑t

source

@[simp]

theorem TopologicalSpace.Clopens.coe_top {α : Type u_2} [TopologicalSpace α] :

↑⊤ = Set.univ

source

@[simp]

theorem TopologicalSpace.Clopens.coe_bot {α : Type u_2} [TopologicalSpace α] :

↑⊥ = ∅

source

@[simp]

theorem TopologicalSpace.Clopens.coe_sdiff {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Clopens α) (t : TopologicalSpace.Clopens α) :

↑(s \ t) = ↑s \ ↑t

source

@[simp]

theorem TopologicalSpace.Clopens.coe_compl {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Clopens α) :

↑sᶜ = (↑s)ᶜ

source

instance TopologicalSpace.Clopens.instInhabitedClopens {α : Type u_2} [TopologicalSpace α] :

Inhabited (TopologicalSpace.Clopens α)