Documentation

Mathlib.Topology.Sets.Closeds

Closed sets #

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

Main Definitions #

For a topological space α,

Closed sets #

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

The type of closed subsets of a topological space.

Instances For

    See Note [custom simps projection].

    Instances For
      @[simp]
      theorem TopologicalSpace.Closeds.coe_mk {α : Type u_2} [TopologicalSpace α] (s : Set α) (h : IsClosed s) :
      { carrier := s, closed' := h } = s

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

      Instances For
        theorem TopologicalSpace.Closeds.gc {α : Type u_2} [TopologicalSpace α] :
        GaloisConnection TopologicalSpace.Closeds.closure SetLike.coe
        def TopologicalSpace.Closeds.gi {α : Type u_2} [TopologicalSpace α] :
        GaloisInsertion TopologicalSpace.Closeds.closure SetLike.coe

        The galois coinsertion between sets and opens.

        Instances For

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

          @[simp]
          @[simp]
          @[simp]
          theorem TopologicalSpace.Closeds.coe_top {α : Type u_2} [TopologicalSpace α] :
          = Set.univ
          @[simp]
          @[simp]
          theorem TopologicalSpace.Closeds.coe_sInf {α : Type u_2} [TopologicalSpace α] {S : Set (TopologicalSpace.Closeds α)} :
          ↑(sInf S) = ⋂ (i : TopologicalSpace.Closeds α) (_ : i S), i
          @[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)
          @[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)
          @[simp]
          theorem TopologicalSpace.Closeds.mem_sInf {α : Type u_2} [TopologicalSpace α] {S : Set (TopologicalSpace.Closeds α)} {x : α} :
          x sInf S ∀ (s : TopologicalSpace.Closeds α), s Sx s
          @[simp]
          theorem TopologicalSpace.Closeds.mem_iInf {α : Type u_2} [TopologicalSpace α] {ι : Sort u_4} {x : α} {s : ιTopologicalSpace.Closeds α} :
          x iInf s ∀ (i : ι), x s i
          @[simp]
          theorem TopologicalSpace.Closeds.coe_iInf {α : Type u_2} [TopologicalSpace α] {ι : Sort u_4} (s : ιTopologicalSpace.Closeds α) :
          ↑(⨅ (i : ι), s i) = ⋂ (i : ι), ↑(s i)
          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))) }
          @[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)) }

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

          Instances For

            The complement of a closed set as an open set.

            Instances For

              The complement of an open set as a closed set.

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

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

                Clopen sets #

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

                The type of clopen sets of a topological space.

                Instances For

                  See Note [custom simps projection].

                  Instances For

                    Reinterpret a clopen as an open.

                    Instances For
                      @[simp]
                      theorem TopologicalSpace.Clopens.coe_mk {α : Type u_2} [TopologicalSpace α] (s : Set α) (h : IsClopen s) :
                      { carrier := s, clopen' := h } = s
                      @[simp]
                      @[simp]
                      @[simp]
                      theorem TopologicalSpace.Clopens.coe_top {α : Type u_2} [TopologicalSpace α] :
                      = Set.univ
                      @[simp]