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.

  • carrier : Set α

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

  • closed' : IsClosed self.carrier
Instances For
    Equations
    • TopologicalSpace.Closeds.instSetLike = { coe := TopologicalSpace.Closeds.carrier, coe_injective' := }
    Equations
    • =

    See Note [custom simps projection].

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

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

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

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

          Equations
          • TopologicalSpace.Closeds.instInhabited = { default := }
          @[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) = iS, i
          @[simp]
          theorem TopologicalSpace.Closeds.coe_sSup {α : Type u_2} [TopologicalSpace α] {S : Set (TopologicalSpace.Closeds α)} :
          (sSup S) = closure (⋃₀ (SetLike.coe '' S))
          @[simp]
          theorem TopologicalSpace.Closeds.coe_finset_sup {ι : Type u_1} {α : Type u_2} [TopologicalSpace α] (f : ιTopologicalSpace.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 : ιTopologicalSpace.Closeds α) (s : Finset ι) :
          (s.inf f) = s.inf (SetLike.coe f)
          @[simp]
          theorem TopologicalSpace.Closeds.mem_sInf {α : Type u_2} [TopologicalSpace α] {S : Set (TopologicalSpace.Closeds α)} {x : α} :
          x sInf S sS, x 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' := }
          @[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' := } = { carrier := ⋂ (i : ι), s i, closed' := }

          Closed sets in a topological space form a coframe.

          Equations
          Instances For
            Equations

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

            Equations
            Instances For
              @[simp]
              theorem TopologicalSpace.Closeds.compl_coe {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Closeds α) :
              s.compl = (s)

              The complement of a closed set as an open set.

              Equations
              • s.compl = { carrier := (s), is_open' := }
              Instances For
                @[simp]
                theorem TopologicalSpace.Opens.coe_compl {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Opens α) :
                s.compl = (s)

                The complement of an open set as a closed set.

                Equations
                • s.compl = { carrier := (s), closed' := }
                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
                  @[simp]
                  theorem TopologicalSpace.Closeds.complOrderIso_apply (α : Type u_2) [TopologicalSpace α] :
                  ∀ (a : TopologicalSpace.Closeds α), (TopologicalSpace.Closeds.complOrderIso α) a = (OrderDual.toDual TopologicalSpace.Closeds.compl) a
                  @[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

                  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
                    @[simp]
                    theorem TopologicalSpace.Opens.complOrderIso_apply (α : Type u_2) [TopologicalSpace α] :
                    ∀ (a : TopologicalSpace.Opens α), (TopologicalSpace.Opens.complOrderIso α) a = (OrderDual.toDual TopologicalSpace.Opens.compl) a
                    @[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

                    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
                      theorem TopologicalSpace.Closeds.coe_eq_singleton_of_isAtom {α : Type u_2} [TopologicalSpace α] [T0Space α] {s : TopologicalSpace.Closeds α} (hs : IsAtom s) :
                      ∃ (a : α), s = {a}

                      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.

                      • carrier : Set α

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

                      • isClopen' : IsClopen self.carrier
                      Instances For
                        Equations

                        See Note [custom simps projection].

                        Equations
                        Instances For
                          @[simp]
                          theorem TopologicalSpace.Clopens.toOpens_coe {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Clopens α) :
                          s.toOpens = s

                          Reinterpret a clopen as an open.

                          Equations
                          • s.toOpens = { carrier := s, is_open' := }
                          Instances For
                            @[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
                            Equations
                            Equations
                            Equations
                            • TopologicalSpace.Clopens.instTop = { top := { carrier := , isClopen' := } }
                            Equations
                            • TopologicalSpace.Clopens.instBot = { bot := { carrier := , isClopen' := } }
                            Equations
                            • TopologicalSpace.Clopens.instSDiff = { sdiff := fun (s t : TopologicalSpace.Clopens α) => { carrier := s \ t, isClopen' := } }
                            Equations
                            Equations
                            @[simp]
                            @[simp]
                            @[simp]
                            theorem TopologicalSpace.Clopens.coe_top {α : Type u_2} [TopologicalSpace α] :
                            = Set.univ
                            @[simp]
                            @[simp]
                            Equations
                            Equations
                            • TopologicalSpace.Clopens.instInhabited = { default := }
                            Equations
                            @[simp]
                            theorem TopologicalSpace.Clopens.mem_prod {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {s : TopologicalSpace.Clopens α} {t : TopologicalSpace.Clopens β} {x : α × β} :
                            x s ×ˢ t x.1 s x.2 t

                            Irreducible closed sets #

                            The type of irreducible closed subsets of a topological space.

                            • carrier : Set α

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

                            • is_irreducible' : IsIrreducible self.carrier
                            • is_closed' : IsClosed self.carrier
                            Instances For
                              Equations
                              • TopologicalSpace.IrreducibleCloseds.instSetLike = { coe := TopologicalSpace.IrreducibleCloseds.carrier, coe_injective' := }
                              @[simp]
                              theorem TopologicalSpace.IrreducibleCloseds.coe_mk {α : Type u_2} [TopologicalSpace α] (s : Set α) (h : IsIrreducible s) (h' : IsClosed s) :
                              { carrier := s, is_irreducible' := h, is_closed' := h' } = s

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

                              Equations
                              Instances For
                                @[simp]
                                theorem TopologicalSpace.IrreducibleCloseds.equivSubtype_apply {α : Type u_2} [TopologicalSpace α] (a : TopologicalSpace.IrreducibleCloseds α) :
                                TopologicalSpace.IrreducibleCloseds.equivSubtype a = a.carrier,
                                @[simp]
                                theorem TopologicalSpace.IrreducibleCloseds.equivSubtype_symm_apply {α : Type u_2} [TopologicalSpace α] (a : { x : Set α // IsIrreducible x IsClosed x }) :
                                TopologicalSpace.IrreducibleCloseds.equivSubtype.symm a = { carrier := a, is_irreducible' := , is_closed' := }

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

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem TopologicalSpace.IrreducibleCloseds.equivSubtype'_symm_apply {α : Type u_2} [TopologicalSpace α] (a : { x : Set α // IsClosed x IsIrreducible x }) :
                                  TopologicalSpace.IrreducibleCloseds.equivSubtype'.symm a = { carrier := a, is_irreducible' := , is_closed' := }
                                  @[simp]
                                  theorem TopologicalSpace.IrreducibleCloseds.equivSubtype'_apply {α : Type u_2} [TopologicalSpace α] (a : TopologicalSpace.IrreducibleCloseds α) :
                                  TopologicalSpace.IrreducibleCloseds.equivSubtype' a = a.carrier,

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

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

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

                                    Equations
                                    Instances For

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

                                      Equations
                                      Instances For