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 α) α

Equations

TopologicalSpace.Closeds.instSetLikeCloseds = { coe := TopologicalSpace.Closeds.carrier, coe_injective' := (_ : ∀ (s t : TopologicalSpace.Closeds α), s.carrier = t.carrier → s = t) }

source

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

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

Equations

@TopologicalSpace.Closeds.instCanLiftSetClosedsCoeInstSetLikeClosedsIsClosed = @TopologicalSpace.Closeds.instCanLiftSetClosedsCoeInstSetLikeClosedsIsClosed.proof_1

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].

Equations

TopologicalSpace.Closeds.Simps.coe s = ↑s

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.

Equations

TopologicalSpace.Closeds.closure s = { carrier := closure s, closed' := (_ : IsClosed (closure s)) }

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

CompleteLattice (TopologicalSpace.Closeds α)

Equations

One or more equations did not get rendered due to their size.

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.

Equations

TopologicalSpace.Closeds.instInhabitedCloseds = { default := ⊥ }

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 ∈ 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' := (_ : IsClosed (s i)) } = { carrier := ⋂ i, s i, closed' := (_ : IsClosed (⋂ i, s i)) }

source

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

Order.Coframe (TopologicalSpace.Closeds α)

Equations

One or more equations did not get rendered due to their size.

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.

Equations

TopologicalSpace.Closeds.singleton x = { carrier := {x}, closed' := (_ : IsClosed {x}) }

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.

Equations

TopologicalSpace.Closeds.compl s = { carrier := (↑s)ᶜ, is_open' := (_ : IsOpen s.carrierᶜ) }

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.

Equations

TopologicalSpace.Opens.compl s = { carrier := (↑s)ᶜ, closed' := (_ : IsClosed s.carrierᶜ) }

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 α.

Equations

One or more equations did not get rendered due to their size.

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 α.

Equations

One or more equations did not get rendered due to their size.

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 α) α

Equations

One or more equations did not get rendered due to their size.

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].

Equations

TopologicalSpace.Clopens.Simps.coe s = ↑s

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.

Equations

TopologicalSpace.Clopens.toOpens s = { carrier := ↑s, is_open' := (_ : IsOpen ↑s) }

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 α)

Equations

TopologicalSpace.Clopens.instSupClopens = { sup := fun s t => { carrier := ↑s ∪ ↑t, clopen' := (_ : IsClopen (↑s ∪ ↑t)) } }

source

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

Inf (TopologicalSpace.Clopens α)

Equations

TopologicalSpace.Clopens.instInfClopens = { inf := fun s t => { carrier := ↑s ∩ ↑t, clopen' := (_ : IsClopen (↑s ∩ ↑t)) } }

source

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

Top (TopologicalSpace.Clopens α)

Equations

TopologicalSpace.Clopens.instTopClopens = { top := { carrier := ⊤, clopen' := (_ : IsClopen Set.univ) } }

source

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

Bot (TopologicalSpace.Clopens α)

Equations

TopologicalSpace.Clopens.instBotClopens = { bot := { carrier := ⊥, clopen' := (_ : IsClopen ∅) } }

source

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

SDiff (TopologicalSpace.Clopens α)

Equations

TopologicalSpace.Clopens.instSDiffClopens = { sdiff := fun s t => { carrier := ↑s \ ↑t, clopen' := (_ : IsClopen (↑s \ ↑t)) } }

source

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

HasCompl (TopologicalSpace.Clopens α)

Equations

TopologicalSpace.Clopens.instHasComplClopens = { compl := fun s => { carrier := (↑s)ᶜ, clopen' := (_ : IsClopen (↑s)ᶜ) } }

source

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

BooleanAlgebra (TopologicalSpace.Clopens α)

Equations

One or more equations did not get rendered due to their size.

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 α)

Equations

TopologicalSpace.Clopens.instInhabitedClopens = { default := ⊥ }