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
    Equations
    • TopologicalSpace.Closeds.instSetLikeCloseds = { coe := TopologicalSpace.Closeds.carrier, coe_injective' := }

    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.instInhabitedCloseds = { 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) = ⋂ i ∈ S, 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 ι) :
          (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 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' := }

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

          Equations
          Instances For

            The complement of a closed set as an open set.

            Equations
            Instances For

              The complement of an open set as a closed set.

              Equations
              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_symm_apply (α : Type u_2) [TopologicalSpace α] :
                ∀ (a : (TopologicalSpace.Opens α)ᵒᵈ), (RelIso.symm (TopologicalSpace.Closeds.complOrderIso α)) a = (TopologicalSpace.Opens.compl OrderDual.ofDual) a
                @[simp]
                theorem TopologicalSpace.Closeds.complOrderIso_apply (α : Type u_2) [TopologicalSpace α] :
                ∀ (a : TopologicalSpace.Closeds α), (TopologicalSpace.Closeds.complOrderIso α) a = (OrderDual.toDual TopologicalSpace.Closeds.compl) 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_symm_apply (α : Type u_2) [TopologicalSpace α] :
                  ∀ (a : (TopologicalSpace.Closeds α)ᵒᵈ), (RelIso.symm (TopologicalSpace.Opens.complOrderIso α)) a = (TopologicalSpace.Closeds.compl OrderDual.ofDual) a
                  @[simp]
                  theorem TopologicalSpace.Opens.complOrderIso_apply (α : Type u_2) [TopologicalSpace α] :
                  ∀ (a : TopologicalSpace.Opens α), (TopologicalSpace.Opens.complOrderIso α) a = (OrderDual.toDual TopologicalSpace.Opens.compl) 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.

                    Instances For
                      Equations
                      • TopologicalSpace.Clopens.instSetLikeClopens = { coe := fun (s : TopologicalSpace.Clopens α) => s.carrier, coe_injective' := }

                      See Note [custom simps projection].

                      Equations
                      Instances For

                        Reinterpret a clopen as an open.

                        Equations
                        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
                          • TopologicalSpace.Clopens.instSupClopens = { sup := fun (s t : TopologicalSpace.Clopens α) => { carrier := s t, isClopen' := } }
                          Equations
                          • TopologicalSpace.Clopens.instInfClopens = { inf := fun (s t : TopologicalSpace.Clopens α) => { carrier := s t, isClopen' := } }
                          Equations
                          • TopologicalSpace.Clopens.instTopClopens = { top := { carrier := , isClopen' := } }
                          Equations
                          • TopologicalSpace.Clopens.instBotClopens = { bot := { carrier := , isClopen' := } }
                          Equations
                          • TopologicalSpace.Clopens.instSDiffClopens = { sdiff := fun (s t : TopologicalSpace.Clopens α) => { carrier := s \ t, isClopen' := } }
                          Equations
                          • TopologicalSpace.Clopens.instHasComplClopens = { compl := fun (s : TopologicalSpace.Clopens α) => { carrier := (s), isClopen' := } }
                          Equations
                          @[simp]
                          @[simp]
                          @[simp]
                          theorem TopologicalSpace.Clopens.coe_top {α : Type u_2} [TopologicalSpace α] :
                          = Set.univ
                          @[simp]
                          Equations
                          • TopologicalSpace.Clopens.instInhabitedClopens = { default := }
                          Equations
                          • One or more equations did not get rendered due to their size.
                          @[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