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

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

The type of closed subsets of a topological space.

• carrier : Set α

  the carrier set, i.e. the points in this set

• isClosed' : IsClosed self.carrier

@[implicit_reducible]

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

Equations

• TopologicalSpace.Closeds.instSetLike = { coe := TopologicalSpace.Closeds.carrier, coe_injective := ⋯ }

@[implicit_reducible]

instance TopologicalSpace.Closeds.instPartialOrder {α : Type u_2} [TopologicalSpace α] : PartialOrder (Closeds α)

Equations

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

instance TopologicalSpace.Closeds.instCanLiftSetCoeIsClosed {α : Type u_2} [TopologicalSpace α] : CanLift (Set α) (Closeds α) SetLike.coe IsClosed

theorem TopologicalSpace.Closeds.isClosed {α : Type u_2} [TopologicalSpace α] (s : Closeds α) : IsClosed ↑s

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

See Note [custom simps projection].

Equations

• TopologicalSpace.Closeds.Simps.coe s = ↑s

@[simp]

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

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

theorem TopologicalSpace.Closeds.ext_iff {α : Type u_2} [TopologicalSpace α] {s t : Closeds α} : s = t ↔ ↑s = ↑t

@[simp]

theorem TopologicalSpace.Closeds.coe_mk {α : Type u_2} [TopologicalSpace α] (s : Set α) (h : IsClosed s) : ↑{ carrier := s, isClosed' := h } = s

@[simp]

theorem TopologicalSpace.Closeds.mem_mk {α : Type u_2} [TopologicalSpace α] {s : Set α} {hs : IsClosed s} {x : α} : x ∈ { carrier := s, isClosed' := hs } ↔ x ∈ s

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

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

Equations

• TopologicalSpace.Closeds.closure s = { carrier := closure s, isClosed' := ⋯ }

@[simp]

theorem TopologicalSpace.Closeds.coe_closure {α : Type u_2} [TopologicalSpace α] (s : Set α) : ↑(Closeds.closure s) = closure s

@[simp]

theorem TopologicalSpace.Closeds.mem_closure {α : Type u_2} [TopologicalSpace α] {s : Set α} {x : α} : x ∈ Closeds.closure s ↔ x ∈ closure s

theorem TopologicalSpace.Closeds.gc {α : Type u_2} [TopologicalSpace α] : GaloisConnection Closeds.closure SetLike.coe

@[simp]

theorem TopologicalSpace.Closeds.closure_le {α : Type u_2} [TopologicalSpace α] {s : Set α} {t : Closeds α} : Closeds.closure s ≤ t ↔ s ⊆ ↑t

def TopologicalSpace.Closeds.gi {α : Type u_2} [TopologicalSpace α] : GaloisInsertion Closeds.closure SetLike.coe

The Galois insertion between sets and closeds.

Equations

• TopologicalSpace.Closeds.gi = { choice := fun (s : Set α) (hs : ↑(TopologicalSpace.Closeds.closure s) ≤ s) => { carrier := s, isClosed' := ⋯ }, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

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

Equations

• TopologicalSpace.Closeds.instInhabited = { default := ⊥ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem TopologicalSpace.Closeds.coe_nonempty {α : Type u_2} [TopologicalSpace α] {s : Closeds α} : (↑s).Nonempty ↔ s ≠ ⊥

@[simp]

theorem TopologicalSpace.Closeds.coe_sInf {α : Type u_2} [TopologicalSpace α] {S : Set (Closeds α)} : ↑(sInf S) = ⋂ i ∈ S, ↑i

@[simp]

theorem TopologicalSpace.Closeds.coe_sSup {α : Type u_2} [TopologicalSpace α] {S : Set (Closeds α)} : ↑(sSup S) = closure (⋃₀ (SetLike.coe '' S))

@[simp]

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

@[simp]

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

@[simp]

theorem TopologicalSpace.Closeds.mem_sInf {α : Type u_2} [TopologicalSpace α] {S : Set (Closeds α)} {x : α} : x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

@[simp]

theorem TopologicalSpace.Closeds.mem_iInf {α : Type u_2} [TopologicalSpace α] {ι : Sort u_4} {x : α} {s : ι → Closeds α} : x ∈ iInf s ↔ ∀ (i : ι), x ∈ s i

@[simp]

theorem TopologicalSpace.Closeds.coe_iInf {α : Type u_2} [TopologicalSpace α] {ι : Sort u_4} (s : ι → Closeds α) : ↑(⨅ (i : ι), s i) = ⋂ (i : ι), ↑(s i)

theorem TopologicalSpace.Closeds.iInf_def {α : Type u_2} [TopologicalSpace α] {ι : Sort u_4} (s : ι → Closeds α) : ⨅ (i : ι), s i = { carrier := ⋂ (i : ι), ↑(s i), isClosed' := ⋯ }

@[simp]

theorem TopologicalSpace.Closeds.iInf_mk {α : Type u_2} [TopologicalSpace α] {ι : Sort u_4} (s : ι → Set α) (h : ∀ (i : ι), IsClosed (s i)) : ⨅ (i : ι), { carrier := s i, isClosed' := ⋯ } = { carrier := ⋂ (i : ι), s i, isClosed' := ⋯ }

@[implicit_reducible]

def TopologicalSpace.Closeds.coframeMinimalAxioms {α : Type u_2} [TopologicalSpace α] : Order.Coframe.MinimalAxioms (Closeds α)

Closed sets in a topological space form a coframe.

Equations

• TopologicalSpace.Closeds.coframeMinimalAxioms = { toCompleteLattice := TopologicalSpace.Closeds.instCompleteLattice, iInf_sup_le_sup_sInf := ⋯ }

@[implicit_reducible]

instance TopologicalSpace.Closeds.instCoframe {α : Type u_2} [TopologicalSpace α] : Order.Coframe (Closeds α)

Equations

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

@[implicit_reducible]

instance TopologicalSpace.Closeds.instSingletonOfT1Space {α : Type u_2} [TopologicalSpace α] [T1Space α] : Singleton α (Closeds α)

Equations

• TopologicalSpace.Closeds.instSingletonOfT1Space = { singleton := fun (x : α) => { carrier := {x}, isClosed' := ⋯ } }

@[simp]

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

@[reducible, inline, deprecated "Use `{x}` instead" (since := "2025-11-23")]

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

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

Equations

• TopologicalSpace.Closeds.singleton x = {x}

@[simp]

theorem TopologicalSpace.Closeds.mk_singleton {α : Type u_2} [TopologicalSpace α] [T1Space α] {x : α} : { carrier := {x}, isClosed' := ⋯ } = {x}

@[simp]

theorem TopologicalSpace.Closeds.mem_singleton {α : Type u_2} [TopologicalSpace α] [T1Space α] {a b : α} : a ∈ {b} ↔ a = b

theorem TopologicalSpace.Closeds.singleton_injective {α : Type u_2} [TopologicalSpace α] [T1Space α] : Function.Injective fun (x : α) => {x}

@[simp]

theorem TopologicalSpace.Closeds.singleton_inj {α : Type u_2} [TopologicalSpace α] [T1Space α] {x y : α} : {x} = {y} ↔ x = y

def TopologicalSpace.Closeds.preimage {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (s : Closeds β) {f : α → β} (hf : Continuous f) : Closeds α

The preimage of a closed set under a continuous map.

Equations

• s.preimage hf = { carrier := f ⁻¹' ↑s, isClosed' := ⋯ }

@[simp]

theorem TopologicalSpace.Closeds.coe_preimage {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (s : Closeds β) {f : α → β} (hf : Continuous f) : ↑(s.preimage hf) = f ⁻¹' ↑s

@[implicit_reducible]

instance TopologicalSpace.Closeds.instSProdProd {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] : SProd (Closeds α) (Closeds β) (Closeds (α × β))

Equations

• TopologicalSpace.Closeds.instSProdProd = { sprod := fun (s : TopologicalSpace.Closeds α) (t : TopologicalSpace.Closeds β) => { carrier := ↑s ×ˢ ↑t, isClosed' := ⋯ } }

@[simp]

theorem TopologicalSpace.Closeds.coe_prod {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (s : Closeds α) (t : Closeds β) : ↑(s ×ˢ t) = ↑s ×ˢ ↑t

@[simp]

theorem TopologicalSpace.Closeds.mem_prod {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {s : Closeds α} {t : Closeds β} {x : α × β} : x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t

@[simp]

theorem TopologicalSpace.Closeds.singleton_prod_singleton {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [T1Space α] [T1Space β] (x : α) (y : β) : {x} ×ˢ {y} = {(x, y)}

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

The complement of a closed set as an open set.

Equations

• s.compl = { carrier := (↑s)ᶜ, is_open' := ⋯ }

@[simp]

theorem TopologicalSpace.Closeds.coe_compl {α : Type u_2} [TopologicalSpace α] (s : Closeds α) : ↑s.compl = (↑s)ᶜ

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

The complement of an open set as a closed set.

Equations

• s.compl = { carrier := (↑s)ᶜ, isClosed' := ⋯ }

@[simp]

theorem TopologicalSpace.Opens.coe_compl {α : Type u_2} [TopologicalSpace α] (s : Opens α) : ↑s.compl = (↑s)ᶜ

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

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

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

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

def TopologicalSpace.Closeds.complOrderIso (α : Type u_2) [TopologicalSpace α] : Closeds α ≃o (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.

@[simp]

theorem TopologicalSpace.Closeds.complOrderIso_symm_apply (α : Type u_2) [TopologicalSpace α] (a✝ : (Opens α)ᵒᵈ) : (RelIso.symm (complOrderIso α)) a✝ = (Opens.compl ∘ ⇑OrderDual.ofDual) a✝

@[simp]

theorem TopologicalSpace.Closeds.complOrderIso_apply (α : Type u_2) [TopologicalSpace α] (a✝ : Closeds α) : (complOrderIso α) a✝ = (⇑OrderDual.toDual ∘ compl) a✝

def TopologicalSpace.Opens.complOrderIso (α : Type u_2) [TopologicalSpace α] : Opens α ≃o (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.

@[simp]

theorem TopologicalSpace.Opens.complOrderIso_apply (α : Type u_2) [TopologicalSpace α] (a✝ : Opens α) : (complOrderIso α) a✝ = (⇑OrderDual.toDual ∘ compl) a✝

@[simp]

theorem TopologicalSpace.Opens.complOrderIso_symm_apply (α : Type u_2) [TopologicalSpace α] (a✝ : (Closeds α)ᵒᵈ) : (RelIso.symm (complOrderIso α)) a✝ = (Closeds.compl ∘ ⇑OrderDual.ofDual) a✝

theorem TopologicalSpace.Closeds.coe_eq_singleton_of_isAtom {α : Type u_2} [TopologicalSpace α] [T0Space α] {s : Closeds α} (hs : IsAtom s) : ∃ (a : α), ↑s = {a}

@[simp]

theorem TopologicalSpace.Closeds.isAtom_coe {α : Type u_2} [TopologicalSpace α] [T1Space α] {s : Closeds α} : IsAtom ↑s ↔ IsAtom s

theorem TopologicalSpace.Closeds.isAtom_iff {α : Type u_2} [TopologicalSpace α] [T1Space α] {s : Closeds α} : IsAtom s ↔ ∃ (x : α), s = {x}

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

theorem TopologicalSpace.Opens.isCoatom_iff {α : Type u_2} [TopologicalSpace α] [T1Space α] {s : Opens α} : IsCoatom s ↔ ∃ (x : α), s = {x}.compl

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

Clopen sets

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

The type of clopen sets of a topological space.

• carrier : Set α

  the carrier set, i.e. the points in this set

• isClopen' : IsClopen self.carrier

@[implicit_reducible]

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

Equations

• TopologicalSpace.Clopens.instSetLike = { coe := fun (s : TopologicalSpace.Clopens α) => s.carrier, coe_injective := ⋯ }

@[implicit_reducible]

instance TopologicalSpace.Clopens.instPartialOrder {α : Type u_2} [TopologicalSpace α] : PartialOrder (Clopens α)

Equations

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

theorem TopologicalSpace.Clopens.isClopen {α : Type u_2} [TopologicalSpace α] (s : Clopens α) : IsClopen ↑s

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

theorem TopologicalSpace.Clopens.isClosed {α : Type u_2} [TopologicalSpace α] (s : Clopens α) : IsClosed ↑s

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

See Note [custom simps projection].

Equations

• TopologicalSpace.Clopens.Simps.coe s = ↑s

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

Reinterpret a clopen as an open.

Equations

• s.toOpens = { carrier := ↑s, is_open' := ⋯ }

@[simp]

theorem TopologicalSpace.Clopens.coe_toOpens {α : Type u_2} [TopologicalSpace α] (s : Clopens α) : ↑s.toOpens = ↑s

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

Reinterpret a clopen as a closed.

Equations

• s.toCloseds = { carrier := ↑s, isClosed' := ⋯ }

@[simp]

theorem TopologicalSpace.Clopens.coe_toCloseds {α : Type u_2} [TopologicalSpace α] (s : Clopens α) : ↑s.toCloseds = ↑s

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

theorem TopologicalSpace.Clopens.ext_iff {α : Type u_2} [TopologicalSpace α] {s t : Clopens α} : s = t ↔ ↑s = ↑t

@[simp]

theorem TopologicalSpace.Clopens.coe_mk {α : Type u_2} [TopologicalSpace α] (s : Set α) (h : IsClopen s) : ↑{ carrier := s, isClopen' := h } = s

@[simp]

theorem TopologicalSpace.Clopens.mem_mk {α : Type u_2} [TopologicalSpace α] {s : Set α} {x : α} {h : IsClopen s} : x ∈ { carrier := s, isClopen' := h } ↔ x ∈ s

@[implicit_reducible]

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

Equations

• TopologicalSpace.Clopens.instMax = { max := fun (s t : TopologicalSpace.Clopens α) => { carrier := ↑s ∪ ↑t, isClopen' := ⋯ } }

@[implicit_reducible]

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

Equations

• TopologicalSpace.Clopens.instMin = { min := fun (s t : TopologicalSpace.Clopens α) => { carrier := ↑s ∩ ↑t, isClopen' := ⋯ } }

@[implicit_reducible]

instance TopologicalSpace.Clopens.instTop {α : Type u_2} [TopologicalSpace α] : Top (Clopens α)

Equations

• TopologicalSpace.Clopens.instTop = { top := { carrier := ⊤, isClopen' := ⋯ } }

@[implicit_reducible]

instance TopologicalSpace.Clopens.instBot {α : Type u_2} [TopologicalSpace α] : Bot (Clopens α)

Equations

• TopologicalSpace.Clopens.instBot = { bot := { carrier := ⊥, isClopen' := ⋯ } }

@[implicit_reducible]

instance TopologicalSpace.Clopens.instSDiff {α : Type u_2} [TopologicalSpace α] : SDiff (Clopens α)

Equations

• TopologicalSpace.Clopens.instSDiff = { sdiff := fun (s t : TopologicalSpace.Clopens α) => { carrier := ↑s \ ↑t, isClopen' := ⋯ } }

@[implicit_reducible]

instance TopologicalSpace.Clopens.instHImp {α : Type u_2} [TopologicalSpace α] : HImp (Clopens α)

Equations

• TopologicalSpace.Clopens.instHImp = { himp := fun (s t : TopologicalSpace.Clopens α) => { carrier := ↑s ⇨ ↑t, isClopen' := ⋯ } }

@[implicit_reducible]

instance TopologicalSpace.Clopens.instCompl {α : Type u_2} [TopologicalSpace α] : Compl (Clopens α)

Equations

• TopologicalSpace.Clopens.instCompl = { compl := fun (s : TopologicalSpace.Clopens α) => { carrier := (↑s)ᶜ, isClopen' := ⋯ } }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

instance TopologicalSpace.Clopens.instBooleanAlgebra {α : Type u_2} [TopologicalSpace α] : BooleanAlgebra (Clopens α)

Equations

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

@[implicit_reducible]

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

Equations

• TopologicalSpace.Clopens.instInhabited = { default := ⊥ }

@[implicit_reducible]

instance TopologicalSpace.Clopens.instSProdProd {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] : SProd (Clopens α) (Clopens β) (Clopens (α × β))

Equations

• TopologicalSpace.Clopens.instSProdProd = { sprod := fun (s : TopologicalSpace.Clopens α) (t : TopologicalSpace.Clopens β) => { carrier := ↑s ×ˢ ↑t, isClopen' := ⋯ } }

@[simp]

theorem TopologicalSpace.Clopens.mem_prod {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {s : Clopens α} {t : Clopens β} {x : α × β} : x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t

@[simp]

theorem TopologicalSpace.Clopens.coe_finset_sup {ι : Type u_1} {α : Type u_2} [TopologicalSpace α] (s : Finset ι) (U : ι → Clopens α) : ↑(s.sup U) = ⋃ i ∈ s, ↑(U i)

@[simp]

theorem TopologicalSpace.Clopens.coe_disjoint {α : Type u_2} [TopologicalSpace α] {s t : Clopens α} : Disjoint ↑s ↑t ↔ Disjoint s t

Irreducible closed sets

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

The type of irreducible closed subsets of a topological space.

• carrier : Set α

  the carrier set, i.e. the points in this set

• isIrreducible' : IsIrreducible self.carrier
• isClosed' : IsClosed self.carrier

@[implicit_reducible]

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

Equations

• TopologicalSpace.IrreducibleCloseds.instSetLike = { coe := TopologicalSpace.IrreducibleCloseds.carrier, coe_injective := ⋯ }

@[implicit_reducible]

instance TopologicalSpace.IrreducibleCloseds.instPartialOrder {α : Type u_2} [TopologicalSpace α] : PartialOrder (IrreducibleCloseds α)

Equations

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

instance TopologicalSpace.IrreducibleCloseds.instCanLiftSetCoeAndIsIrreducibleIsClosed {α : Type u_2} [TopologicalSpace α] : CanLift (Set α) (IrreducibleCloseds α) SetLike.coe fun (s : Set α) => IsIrreducible s ∧ IsClosed s

theorem TopologicalSpace.IrreducibleCloseds.isIrreducible {α : Type u_2} [TopologicalSpace α] (s : IrreducibleCloseds α) : IsIrreducible ↑s

theorem TopologicalSpace.IrreducibleCloseds.isClosed {α : Type u_2} [TopologicalSpace α] (s : IrreducibleCloseds α) : IsClosed ↑s

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

See Note [custom simps projection].

Equations

• TopologicalSpace.IrreducibleCloseds.Simps.coe s = ↑s

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

theorem TopologicalSpace.IrreducibleCloseds.ext_iff {α : Type u_2} [TopologicalSpace α] {s t : IrreducibleCloseds α} : s = t ↔ ↑s = ↑t

@[simp]

theorem TopologicalSpace.IrreducibleCloseds.coe_mk {α : Type u_2} [TopologicalSpace α] (s : Set α) (h : IsIrreducible s) (h' : IsClosed s) : ↑{ carrier := s, isIrreducible' := h, isClosed' := h' } = s

@[implicit_reducible]

instance TopologicalSpace.IrreducibleCloseds.instSingletonOfT1Space {α : Type u_2} [TopologicalSpace α] [T1Space α] : Singleton α (IrreducibleCloseds α)

Equations

• TopologicalSpace.IrreducibleCloseds.instSingletonOfT1Space = { singleton := fun (x : α) => { carrier := {x}, isIrreducible' := ⋯, isClosed' := ⋯ } }

@[simp]

theorem TopologicalSpace.IrreducibleCloseds.coe_singleton {α : Type u_2} [TopologicalSpace α] [T1Space α] (x : α) : ↑{x} = {x}

@[reducible, inline, deprecated "Use `{x}` instead" (since := "2025-11-23")]

abbrev TopologicalSpace.IrreducibleCloseds.singleton {α : Type u_2} [TopologicalSpace α] [T1Space α] (x : α) : IrreducibleCloseds α

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

Equations

• TopologicalSpace.IrreducibleCloseds.singleton x = {x}

@[simp]

theorem TopologicalSpace.IrreducibleCloseds.mk_singleton {α : Type u_2} [TopologicalSpace α] [T1Space α] {x : α} : { carrier := {x}, isIrreducible' := ⋯, isClosed' := ⋯ } = {x}

@[simp]

theorem TopologicalSpace.IrreducibleCloseds.mem_singleton {α : Type u_2} [TopologicalSpace α] [T1Space α] {a b : α} : a ∈ {b} ↔ a = b

theorem TopologicalSpace.IrreducibleCloseds.singleton_injective {α : Type u_2} [TopologicalSpace α] [T1Space α] : Function.Injective fun (x : α) => {x}

@[simp]

theorem TopologicalSpace.IrreducibleCloseds.singleton_inj {α : Type u_2} [TopologicalSpace α] [T1Space α] {x y : α} : {x} = {y} ↔ x = y

def TopologicalSpace.IrreducibleCloseds.equivSubtype {α : Type u_2} [TopologicalSpace α] : IrreducibleCloseds α ≃ { x : Set α // IsIrreducible x ∧ IsClosed x }

The equivalence between IrreducibleCloseds α and {x : Set α // IsIrreducible x ∧ IsClosed x }.

Equations

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

@[simp]

theorem TopologicalSpace.IrreducibleCloseds.equivSubtype_symm_apply {α : Type u_2} [TopologicalSpace α] (a : { x : Set α // IsIrreducible x ∧ IsClosed x }) : equivSubtype.symm a = { carrier := ↑a, isIrreducible' := ⋯, isClosed' := ⋯ }

@[simp]

theorem TopologicalSpace.IrreducibleCloseds.equivSubtype_apply {α : Type u_2} [TopologicalSpace α] (a : IrreducibleCloseds α) : equivSubtype a = ⟨a.carrier, ⋯⟩

def TopologicalSpace.IrreducibleCloseds.equivSubtype' {α : Type u_2} [TopologicalSpace α] : IrreducibleCloseds α ≃ { x : Set α // IsClosed x ∧ IsIrreducible x }

The equivalence between IrreducibleCloseds α and {x : Set α // IsClosed x ∧ IsIrreducible x }.

Equations

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

@[simp]

theorem TopologicalSpace.IrreducibleCloseds.equivSubtype'_symm_apply {α : Type u_2} [TopologicalSpace α] (a : { x : Set α // IsClosed x ∧ IsIrreducible x }) : equivSubtype'.symm a = { carrier := ↑a, isIrreducible' := ⋯, isClosed' := ⋯ }

@[simp]

theorem TopologicalSpace.IrreducibleCloseds.equivSubtype'_apply {α : Type u_2} [TopologicalSpace α] (a : IrreducibleCloseds α) : equivSubtype' a = ⟨a.carrier, ⋯⟩

def TopologicalSpace.IrreducibleCloseds.orderIsoSubtype (α : Type u_2) [TopologicalSpace α] : IrreducibleCloseds α ≃o { x : Set α // IsIrreducible x ∧ IsClosed x }

The equivalence IrreducibleCloseds α ≃ { x : Set α // IsIrreducible x ∧ IsClosed x } is an order isomorphism.

Equations

• TopologicalSpace.IrreducibleCloseds.orderIsoSubtype α = TopologicalSpace.IrreducibleCloseds.equivSubtype.toOrderIso ⋯ ⋯

def TopologicalSpace.IrreducibleCloseds.orderIsoSubtype' (α : Type u_2) [TopologicalSpace α] : IrreducibleCloseds α ≃o { x : Set α // IsClosed x ∧ IsIrreducible x }

The equivalence IrreducibleCloseds α ≃ { x : Set α // IsClosed x ∧ IsIrreducible x } is an order isomorphism.

Equations

• TopologicalSpace.IrreducibleCloseds.orderIsoSubtype' α = TopologicalSpace.IrreducibleCloseds.equivSubtype'.toOrderIso ⋯ ⋯

Partial order structure on irreducible closed sets and maps thereof.

def TopologicalSpace.IrreducibleCloseds.map {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : β → α) (hf : Continuous f) (c : IrreducibleCloseds β) : IrreducibleCloseds α

The map on irreducible closed sets induced by a continuous map f.

Equations

• TopologicalSpace.IrreducibleCloseds.map f hf c = { carrier := closure (f '' ↑c), isIrreducible' := ⋯, isClosed' := ⋯ }

@[simp]

theorem TopologicalSpace.IrreducibleCloseds.coe_map {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : β → α) (hf : Continuous f) (s : IrreducibleCloseds β) : ↑(map f hf s) = closure (f '' ↑s)

theorem TopologicalSpace.IrreducibleCloseds.map_mono {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : β → α} (hf : Continuous f) : Monotone (map f hf)

theorem TopologicalSpace.IrreducibleCloseds.map_injective_of_isInducing {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : β → α} (hf : Topology.IsInducing f) : Function.Injective (map f ⋯)

The map IrreducibleCloseds.map is injective when f is inducing. This relies on the property of embeddings that a closed set in the domain is the preimage of the closure of its image.

theorem TopologicalSpace.IrreducibleCloseds.map_strictMono_of_isInducing {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : β → α} (hf : Topology.IsInducing f) : StrictMono (map f ⋯)

The map IrreducibleCloseds.map is strictly monotone when f is inducing.

noncomputable def TopologicalSpace.IrreducibleCloseds.orderIsoOfIsOpenEmbedding {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : β → α) (h : Topology.IsOpenEmbedding f) : IrreducibleCloseds β ≃o ↑{V : IrreducibleCloseds α | (f ⁻¹' ↑V).Nonempty}

Given f : U → X a continuous open embedding, the irreducible closeds of U are order isomorphic to the irreducible closeds of X nontrivially intersecting the range of f.

Equations

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