Documentation

Mathlib.Topology.Order

Ordering on topologies and (co)induced topologies #

Topologies on a fixed type α are ordered, by reverse inclusion. That is, for topologies t₁ and t₂ on α, we write t₁ ≤ t₂≤ t₂ if every set open in t₂ is also open in t₁. (One also calls t₁ finer than t₂, and t₂ coarser than t₁.)

Any function f : α → β→ β induces

Continuity, the ordering on topologies and (co)induced topologies are related as follows:

Topologies on α form a complete lattice, with ⊥⊥ the discrete topology and ⊤⊤ the indiscrete topology.

For a function f : α → β→ β, (TopologicalSpace.coinduced f, TopologicalSpace.induced f) is a Galois connection between topologies on α and topologies on β.

Implementation notes #

There is a Galois insertion between topologies on α (with the inclusion ordering) and all collections of sets in α. The complete lattice structure on topologies on α is defined as the reverse of the one obtained via this Galois insertion. More precisely, we use the corresponding Galois coinsertion between topologies on α (with the reversed inclusion ordering) and collections of sets in α (with the reversed inclusion ordering).

Tags #

finer, coarser, induced topology, coinduced topology

inductive TopologicalSpace.GenerateOpen {α : Type u} (g : Set (Set α)) :
Set αProp

The open sets of the least topology containing a collection of basic sets.

Instances For

    The smallest topological space containing the collection g of basic sets

    Equations
    • One or more equations did not get rendered due to their size.
    theorem TopologicalSpace.isOpen_generateFrom_of_mem {α : Type u} {g : Set (Set α)} {s : Set α} (hs : s g) :
    theorem TopologicalSpace.nhds_generateFrom {α : Type u} {g : Set (Set α)} {a : α} :
    nhds a = s, h, Filter.principal s
    theorem TopologicalSpace.tendsto_nhds_generateFrom {α : Type u} {β : Type u_1} {m : αβ} {f : Filter α} {g : Set (Set β)} {b : β} (h : ∀ (s : Set β), s gb sm ⁻¹' s f) :
    def TopologicalSpace.mkOfNhds {α : Type u} (n : αFilter α) :

    Construct a topology on α given the filter of neighborhoods of each point of α.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem TopologicalSpace.nhds_mkOfNhds {α : Type u} (n : αFilter α) (a : α) (h₀ : pure n) (h₁ : ∀ (a : α) (s : Set α), s n at, t n a t s ∀ (a' : α), a' ts n a') :
    nhds a = n a
    theorem TopologicalSpace.nhds_mkOfNhds_single {α : Type u} [inst : DecidableEq α] {a₀ : α} {l : Filter α} (h : pure a₀ l) (b : α) :
    nhds b = Function.update pure a₀ l b
    theorem TopologicalSpace.nhds_mkOfNhds_filterBasis {α : Type u} (B : αFilterBasis α) (a : α) (h₀ : ∀ (x : α) (n : Set α), n B xx n) (h₁ : ∀ (x : α) (n : Set α), n B xn₁, n₁ B x n₁ n ∀ (x' : α), x' n₁n₂, n₂ B x' n₂ n) :

    The ordering on topologies on the type α. t ≤ s≤ s if every set open in s is also open in t (t is finer than s).

    Equations
    • One or more equations did not get rendered due to their size.
    theorem TopologicalSpace.le_def {α : Type u_1} {t : TopologicalSpace α} {s : TopologicalSpace α} :
    t s IsOpen IsOpen

    If s equals the collection of open sets in the topology it generates, then s defines a topology.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem TopologicalSpace.gc_generateFrom (α : Type u_1) :
    GaloisConnection (fun t => OrderDual.toDual { s | IsOpen s }) (TopologicalSpace.generateFrom OrderDual.ofDual)
    def TopologicalSpace.gciGenerateFrom (α : Type u_1) :
    GaloisCoinsertion (fun t => OrderDual.toDual { s | IsOpen s }) (TopologicalSpace.generateFrom OrderDual.ofDual)

    The Galois coinsertion between TopologicalSpace α and (Set (Set α))ᵒᵈ whose lower part sends a topology to its collection of open subsets, and whose upper part sends a collection of subsets of α to the topology they generate.

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

    Topologies on α form a complete lattice, with ⊥⊥ the discrete topology and ⊤⊤ the indiscrete topology. The infimum of a collection of topologies is the topology generated by all their open sets, while the supremum is the topology whose open sets are those sets open in every member of the collection.

    Equations
    theorem TopologicalSpace.generateFrom_anti {α : Type u_1} {g₁ : Set (Set α)} {g₂ : Set (Set α)} (h : g₁ g₂) :
    theorem TopologicalSpace.leftInverse_generateFrom {α : Type u} :
    Function.LeftInverse TopologicalSpace.generateFrom fun t => { s | IsOpen s }
    theorem TopologicalSpace.generateFrom_surjective {α : Type u} :
    Function.Surjective TopologicalSpace.generateFrom
    theorem IsOpen.mono {α : Type u_1} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {s : Set α} (hs : IsOpen s) (h : t₁ t₂) :
    theorem IsClosed.mono {α : Type u_1} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {s : Set α} (hs : IsClosed s) (h : t₁ t₂) :
    theorem isOpen_implies_isOpen_iff {α : Type u_1} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} :
    (∀ (s : Set α), IsOpen sIsOpen s) t₂ t₁
    theorem TopologicalSpace.isOpen_top_iff {α : Type u_1} (U : Set α) :
    IsOpen U U = U = Set.univ

    The only open sets in the indiscrete topology are the empty set and the whole space.

    class DiscreteTopology (α : Type u_1) [t : TopologicalSpace α] :

    A topological space is discrete if every set is open, that is, its topology equals the discrete topology ⊥⊥.

    Instances
      @[simp]
      theorem isOpen_discrete {α : Type u_1} [inst : TopologicalSpace α] [inst : DiscreteTopology α] (s : Set α) :
      @[simp]
      theorem isClosed_discrete {α : Type u_1} [inst : TopologicalSpace α] [inst : DiscreteTopology α] (s : Set α) :
      theorem continuous_of_discreteTopology {α : Type u_2} {β : Type u_1} [inst : TopologicalSpace α] [inst : DiscreteTopology α] [inst : TopologicalSpace β] {f : αβ} :
      @[simp]
      theorem nhds_discrete (α : Type u_1) [inst : TopologicalSpace α] [inst : DiscreteTopology α] :
      nhds = pure
      theorem mem_nhds_discrete {α : Type u_1} [inst : TopologicalSpace α] [inst : DiscreteTopology α] {x : α} {s : Set α} :
      s nhds x x s
      theorem le_of_nhds_le_nhds {α : Type u_1} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} (h : ∀ (x : α), nhds x nhds x) :
      t₁ t₂
      theorem eq_of_nhds_eq_nhds {α : Type u_1} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} (h : ∀ (x : α), nhds x = nhds x) :
      t₁ = t₂
      theorem eq_bot_of_singletons_open {α : Type u_1} {t : TopologicalSpace α} (h : ∀ (x : α), IsOpen {x}) :
      t =
      theorem forall_open_iff_discrete {X : Type u_1} [inst : TopologicalSpace X] :
      (∀ (s : Set X), IsOpen s) DiscreteTopology X
      theorem singletons_open_iff_discrete {X : Type u_1} [inst : TopologicalSpace X] :
      (∀ (a : X), IsOpen {a}) DiscreteTopology X
      theorem discreteTopology_iff_nhds {α : Type u_1} [inst : TopologicalSpace α] :
      DiscreteTopology α ∀ (x : α), nhds x = pure x

      This lemma characterizes discrete topological spaces as those whose singletons are neighbourhoods.

      theorem discreteTopology_iff_nhds_ne {α : Type u_1} [inst : TopologicalSpace α] :
      DiscreteTopology α ∀ (x : α), nhdsWithin x ({x}) =
      def TopologicalSpace.induced {α : Type u} {β : Type v} (f : αβ) (t : TopologicalSpace β) :

      Given f : α → β→ β and a topology on β, the induced topology on α is the collection of sets that are preimages of some open set in β. This is the coarsest topology that makes f continuous.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem isOpen_induced_iff {α : Type u_2} {β : Type u_1} [t : TopologicalSpace β] {s : Set α} {f : αβ} :
      IsOpen s t, IsOpen t f ⁻¹' t = s
      theorem isClosed_induced_iff {α : Type u_2} {β : Type u_1} [t : TopologicalSpace β] {s : Set α} {f : αβ} :
      IsClosed s t, IsClosed t f ⁻¹' t = s
      def TopologicalSpace.coinduced {α : Type u} {β : Type v} (f : αβ) (t : TopologicalSpace α) :

      Given f : α → β→ β and a topology on α, the coinduced topology on β is defined such that s : Set β is open if the preimage of s is open. This is the finest topology that makes f continuous.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem isOpen_coinduced {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {s : Set β} {f : αβ} :
      theorem preimage_nhds_coinduced {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {π : αβ} {s : Set β} {a : α} (hs : s nhds (π a)) :
      π ⁻¹' s nhds a
      theorem Continuous.coinduced_le {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {t' : TopologicalSpace β} {f : αβ} (h : Continuous f) :
      theorem coinduced_le_iff_le_induced {α : Type u_1} {β : Type u_2} {f : αβ} {tα : TopologicalSpace α} {tβ : TopologicalSpace β} :
      theorem Continuous.le_induced {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {t' : TopologicalSpace β} {f : αβ} (h : Continuous f) :
      theorem induced_mono {α : Type u_1} {β : Type u_2} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {g : βα} (h : t₁ t₂) :
      theorem coinduced_mono {α : Type u_1} {β : Type u_2} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {f : αβ} (h : t₁ t₂) :
      @[simp]
      theorem induced_top {α : Type u_2} {β : Type u_1} {g : βα} :
      @[simp]
      theorem induced_inf {α : Type u_2} {β : Type u_1} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {g : βα} :
      @[simp]
      theorem induced_infᵢ {α : Type u_1} {β : Type u_2} {g : βα} {ι : Sort w} {t : ιTopologicalSpace α} :
      @[simp]
      theorem coinduced_bot {α : Type u_2} {β : Type u_1} {f : αβ} :
      @[simp]
      theorem coinduced_sup {α : Type u_2} {β : Type u_1} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {f : αβ} :
      @[simp]
      theorem coinduced_supᵢ {α : Type u_1} {β : Type u_2} {f : αβ} {ι : Sort w} {t : ιTopologicalSpace α} :
      theorem induced_compose {α : Type u_2} {β : Type u_3} {γ : Type u_1} [tγ : TopologicalSpace γ] {f : αβ} {g : βγ} :
      theorem induced_const {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] {x : α} :
      theorem coinduced_compose {α : Type u_1} {β : Type u_3} {γ : Type u_2} [tα : TopologicalSpace α] {f : αβ} {g : βγ} :
      Equations
      • inhabitedTopologicalSpace = { default := }
      Equations
      • Subsingleton.uniqueTopologicalSpace = { toInhabited := { default := }, uniq := (_ : ∀ (t : TopologicalSpace α), t = ) }
      Equations
      • instTopologicalSpaceFin =
      theorem continuous_empty_function {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst : TopologicalSpace β] [inst : IsEmpty β] (f : αβ) :
      theorem le_generateFrom {α : Type u} {t : TopologicalSpace α} {g : Set (Set α)} (h : ∀ (s : Set α), s gIsOpen s) :
      theorem le_induced_generateFrom {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] {b : Set (Set β)} {f : αβ} (h : ∀ (a : Set β), a bIsOpen (f ⁻¹' a)) :
      def nhdsAdjoint {α : Type u} (a : α) (f : Filter α) :

      This construction is left adjoint to the operation sending a topology on α to its neighborhood filter at a fixed point a : α.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem gc_nhds {α : Type u} (a : α) :
      theorem nhds_mono {α : Type u} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {a : α} (h : t₁ t₂) :
      theorem le_iff_nhds {α : Type u_1} (t : TopologicalSpace α) (t' : TopologicalSpace α) :
      t t' ∀ (x : α), nhds x nhds x
      theorem nhdsAdjoint_nhds {α : Type u_1} (a : α) (f : Filter α) :
      nhds a = pure a f
      theorem nhdsAdjoint_nhds_of_ne {α : Type u_1} (a : α) (f : Filter α) {b : α} (h : b a) :
      nhds b = pure b
      theorem isOpen_singleton_nhdsAdjoint {α : Type u_1} {a : α} {b : α} (f : Filter α) (hb : b a) :
      IsOpen {b}
      theorem le_nhdsAdjoint_iff' {α : Type u_1} (a : α) (f : Filter α) (t : TopologicalSpace α) :
      t nhdsAdjoint a f nhds a pure a f ∀ (b : α), b anhds b = pure b
      theorem le_nhdsAdjoint_iff {α : Type u_1} (a : α) (f : Filter α) (t : TopologicalSpace α) :
      t nhdsAdjoint a f nhds a pure a f ∀ (b : α), b aIsOpen {b}
      theorem nhds_infᵢ {α : Type u} {ι : Sort u_1} {t : ιTopologicalSpace α} {a : α} :
      nhds a = i, nhds a
      theorem nhds_infₛ {α : Type u} {s : Set (TopologicalSpace α)} {a : α} :
      nhds a = t, h, nhds a
      theorem nhds_inf {α : Type u} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {a : α} :
      theorem nhds_top {α : Type u} {a : α} :
      theorem isOpen_sup {α : Type u} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {s : Set α} :
      theorem continuous_iff_coinduced_le {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} :
      theorem continuous_iff_le_induced {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} :
      theorem continuous_generateFrom {α : Type u} {β : Type v} {f : αβ} {t : TopologicalSpace α} {b : Set (Set β)} (h : ∀ (s : Set β), s bIsOpen (f ⁻¹' s)) :
      theorem continuous_induced_dom {α : Type u} {β : Type v} {f : αβ} {t : TopologicalSpace β} :
      theorem continuous_induced_rng {α : Type u} {β : Type v} {γ : Type u_1} {f : αβ} {g : γα} {t₂ : TopologicalSpace β} {t₁ : TopologicalSpace γ} :
      theorem continuous_coinduced_rng {α : Type u} {β : Type v} {f : αβ} {t : TopologicalSpace α} :
      theorem continuous_coinduced_dom {α : Type u} {β : Type v} {γ : Type u_1} {f : αβ} {g : βγ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace γ} :
      theorem continuous_le_dom {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} (h₁ : t₂ t₁) (h₂ : Continuous f) :
      theorem continuous_le_rng {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} {t₃ : TopologicalSpace β} (h₁ : t₂ t₃) (h₂ : Continuous f) :
      theorem continuous_sup_dom {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
      theorem continuous_sup_rng_left {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₃ : TopologicalSpace β} {t₂ : TopologicalSpace β} :
      theorem continuous_sup_rng_right {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₃ : TopologicalSpace β} {t₂ : TopologicalSpace β} :
      theorem continuous_supₛ_dom {α : Type u} {β : Type v} {f : αβ} {T : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} :
      Continuous f ∀ (t : TopologicalSpace α), t TContinuous f
      theorem continuous_supₛ_rng {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₂ : Set (TopologicalSpace β)} {t : TopologicalSpace β} (h₁ : t t₂) (hf : Continuous f) :
      theorem continuous_supᵢ_dom {α : Type u} {β : Type v} {f : αβ} {ι : Sort u_1} {t₁ : ιTopologicalSpace α} {t₂ : TopologicalSpace β} :
      Continuous f ∀ (i : ι), Continuous f
      theorem continuous_supᵢ_rng {α : Type u} {β : Type v} {f : αβ} {ι : Sort u_1} {t₁ : TopologicalSpace α} {t₂ : ιTopologicalSpace β} {i : ι} (h : Continuous f) :
      theorem continuous_inf_rng {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} {t₃ : TopologicalSpace β} :
      theorem continuous_inf_dom_left {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
      theorem continuous_inf_dom_right {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
      theorem continuous_infₛ_dom {α : Type u} {β : Type v} {f : αβ} {t₁ : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} {t : TopologicalSpace α} (h₁ : t t₁) :
      theorem continuous_infₛ_rng {α : Type u} {β : Type v} {f : αβ} {t₁ : TopologicalSpace α} {T : Set (TopologicalSpace β)} :
      Continuous f ∀ (t : TopologicalSpace β), t TContinuous f
      theorem continuous_infᵢ_dom {α : Type u} {β : Type v} {f : αβ} {ι : Sort u_1} {t₁ : ιTopologicalSpace α} {t₂ : TopologicalSpace β} {i : ι} :
      theorem continuous_infᵢ_rng {α : Type u} {β : Type v} {f : αβ} {ι : Sort u_1} {t₁ : TopologicalSpace α} {t₂ : ιTopologicalSpace β} :
      Continuous f ∀ (i : ι), Continuous f
      theorem continuous_bot {α : Type u} {β : Type v} {f : αβ} {t : TopologicalSpace β} :
      theorem continuous_top {α : Type u} {β : Type v} {f : αβ} {t : TopologicalSpace α} :
      theorem continuous_id_of_le {α : Type u} {t : TopologicalSpace α} {t' : TopologicalSpace α} (h : t t') :
      theorem mem_nhds_induced {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : βα) (a : β) (s : Set β) :
      s nhds a u, u nhds (f a) f ⁻¹' u s
      theorem nhds_induced {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : βα) (a : β) :
      nhds a = Filter.comap f (nhds (f a))
      theorem induced_iff_nhds_eq {α : Type u} {β : Type v} [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : βα) :
      = TopologicalSpace.induced f ∀ (b : β), nhds b = Filter.comap f (nhds (f b))
      theorem map_nhds_induced_of_surjective {α : Type u} {β : Type v} [T : TopologicalSpace α] {f : βα} (hf : Function.Surjective f) (a : β) :
      Filter.map f (nhds a) = nhds (f a)
      theorem isOpen_induced_eq {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : αβ} {s : Set α} :
      theorem isOpen_induced {α : Type u_2} {β : Type u_1} [t : TopologicalSpace β] {f : αβ} {s : Set β} (h : IsOpen s) :
      theorem map_nhds_induced_eq {α : Type u_2} {β : Type u_1} [t : TopologicalSpace β] {f : αβ} (a : α) :
      theorem map_nhds_induced_of_mem {α : Type u_2} {β : Type u_1} [t : TopologicalSpace β] {f : αβ} {a : α} (h : Set.range f nhds (f a)) :
      Filter.map f (nhds a) = nhds (f a)
      theorem closure_induced {α : Type u_2} {β : Type u_1} [t : TopologicalSpace β] {f : αβ} {a : α} {s : Set α} :
      a closure s f a closure (f '' s)
      theorem isClosed_induced_iff' {α : Type u_2} {β : Type u_1} [t : TopologicalSpace β] {f : αβ} {s : Set α} :
      IsClosed s ∀ (a : α), f a closure (f '' s)a s
      theorem tendsto_nhds_true {α : Type u_1} {l : Filter α} {p : αProp} :
      theorem tendsto_nhds_Prop {α : Type u_1} {l : Filter α} {p : αProp} {q : Prop} :
      Filter.Tendsto p l (nhds q) qFilter.Eventually (fun x => p x) l
      theorem continuous_Prop {α : Type u_1} [inst : TopologicalSpace α] {p : αProp} :
      Continuous p IsOpen { x | p x }
      theorem isOpen_iff_continuous_mem {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :
      IsOpen s Continuous fun x => x s
      theorem setOf_isOpen_sup {α : Type u} (t₁ : TopologicalSpace α) (t₂ : TopologicalSpace α) :
      { s | IsOpen s } = { s | IsOpen s } { s | IsOpen s }
      theorem generateFrom_unionᵢ {α : Type u} {ι : Sort v} {f : ιSet (Set α)} :
      theorem setOf_isOpen_supᵢ {α : Type u} {ι : Sort v} {t : ιTopologicalSpace α} :
      { s | IsOpen s } = Set.interᵢ fun i => { s | IsOpen s }
      theorem setOf_isOpen_supₛ {α : Type u} {T : Set (TopologicalSpace α)} :
      { s | IsOpen s } = Set.interᵢ fun t => Set.interᵢ fun h => { s | IsOpen s }
      theorem generateFrom_unionᵢ_isOpen {α : Type u} {ι : Sort v} (f : ιTopologicalSpace α) :
      TopologicalSpace.generateFrom (Set.unionᵢ fun i => { s | IsOpen s }) = i, f i
      theorem generateFrom_interᵢ {α : Type u} {ι : Sort v} (f : ιTopologicalSpace α) :
      TopologicalSpace.generateFrom (Set.interᵢ fun i => { s | IsOpen s }) = i, f i
      theorem generateFrom_interᵢ_of_generateFrom_eq_self {α : Type u} {ι : Sort v} (f : ιSet (Set α)) (hf : ∀ (i : ι), { s | IsOpen s } = f i) :
      theorem isOpen_supᵢ_iff {α : Type u} {ι : Sort v} {t : ιTopologicalSpace α} {s : Set α} :
      IsOpen s ∀ (i : ι), IsOpen s
      theorem isClosed_supᵢ_iff {α : Type u} {ι : Sort v} {t : ιTopologicalSpace α} {s : Set α} :
      IsClosed s ∀ (i : ι), IsClosed s