Documentation

Mathlib.Topology.Sets.Compacts

Compact sets #

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

Main Definitions #

For a topological space α,

Compact sets #

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

The type of compact sets of a topological space.

  • carrier : Set α

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

  • isCompact' : IsCompact self.carrier
Instances For
    Equations
    • TopologicalSpace.Compacts.instSetLike = { coe := TopologicalSpace.Compacts.carrier, coe_injective' := }

    See Note [custom simps projection].

    Equations
    Instances For
      Equations
      • =
      @[simp]
      theorem TopologicalSpace.Compacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : Set α) (h : IsCompact s) :
      { carrier := s, isCompact' := h } = s
      Equations
      Equations
      • TopologicalSpace.Compacts.instInfOfT2Space = { inf := fun (s t : TopologicalSpace.Compacts α) => { carrier := s t, isCompact' := } }
      Equations
      • TopologicalSpace.Compacts.instTopOfCompactSpace = { top := { carrier := Set.univ, isCompact' := } }
      Equations
      • TopologicalSpace.Compacts.instBot = { bot := { carrier := , isCompact' := } }
      Equations
      Equations
      Equations
      • TopologicalSpace.Compacts.instOrderBot = OrderBot.lift SetLike.coe
      Equations
      • TopologicalSpace.Compacts.instBoundedOrderOfCompactSpace = BoundedOrder.lift SetLike.coe

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

      Equations
      • TopologicalSpace.Compacts.instInhabited = { default := }
      @[simp]
      @[simp]
      theorem TopologicalSpace.Compacts.coe_top {α : Type u_1} [TopologicalSpace α] [CompactSpace α] :
      = Set.univ
      @[simp]
      theorem TopologicalSpace.Compacts.coe_finset_sup {α : Type u_1} [TopologicalSpace α] {ι : Type u_4} {s : Finset ι} {f : ιTopologicalSpace.Compacts α} :
      (s.sup f) = s.sup fun (i : ι) => (f i)

      The image of a compact set under a continuous function.

      Equations
      Instances For
        @[simp]
        theorem TopologicalSpace.Compacts.coe_map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : Continuous f) (s : TopologicalSpace.Compacts α) :

        A homeomorphism induces an equivalence on compact sets, by taking the image.

        Equations
        Instances For

          The image of a compact set under a homeomorphism can also be expressed as a preimage.

          The product of two TopologicalSpace.Compacts, as a TopologicalSpace.Compacts in the product space.

          Equations
          • K.prod L = { carrier := K ×ˢ L, isCompact' := }
          Instances For
            @[simp]
            theorem TopologicalSpace.Compacts.coe_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (K : TopologicalSpace.Compacts α) (L : TopologicalSpace.Compacts β) :
            (K.prod L) = K ×ˢ L

            Nonempty compact sets #

            The type of nonempty compact sets of a topological space.

            • carrier : Set α
            • isCompact' : IsCompact self.carrier
            • nonempty' : self.carrier.Nonempty
            Instances For
              Equations

              See Note [custom simps projection].

              Equations
              Instances For

                Reinterpret a nonempty compact as a closed set.

                Equations
                • s.toCloseds = { carrier := s, closed' := }
                Instances For
                  @[simp]
                  theorem TopologicalSpace.NonemptyCompacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : s.carrier.Nonempty) :
                  { toCompacts := s, nonempty' := h } = s
                  Equations
                  Equations
                  • TopologicalSpace.NonemptyCompacts.instTopOfCompactSpaceOfNonempty = { top := { toCompacts := , nonempty' := } }
                  Equations
                  Equations
                  • TopologicalSpace.NonemptyCompacts.instOrderTopOfCompactSpaceOfNonempty = OrderTop.lift SetLike.coe
                  @[simp]

                  In an inhabited space, the type of nonempty compact subsets is also inhabited, with default element the singleton set containing the default element.

                  Equations
                  • TopologicalSpace.NonemptyCompacts.instInhabited = { default := { carrier := {default}, isCompact' := , nonempty' := } }

                  The product of two TopologicalSpace.NonemptyCompacts, as a TopologicalSpace.NonemptyCompacts in the product space.

                  Equations
                  • K.prod L = { toCompacts := K.prod L.toCompacts, nonempty' := }
                  Instances For

                    Positive compact sets #

                    The type of compact sets with nonempty interior of a topological space. See also TopologicalSpace.Compacts and TopologicalSpace.NonemptyCompacts.

                    • carrier : Set α
                    • isCompact' : IsCompact self.carrier
                    • interior_nonempty' : (interior self.carrier).Nonempty
                    Instances For
                      Equations

                      See Note [custom simps projection].

                      Equations
                      Instances For

                        Reinterpret a positive compact as a nonempty compact.

                        Equations
                        • s.toNonemptyCompacts = { toCompacts := s.toCompacts, nonempty' := }
                        Instances For
                          @[simp]
                          theorem TopologicalSpace.PositiveCompacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : (interior s.carrier).Nonempty) :
                          { toCompacts := s, interior_nonempty' := h } = s
                          Equations
                          Equations
                          • TopologicalSpace.PositiveCompacts.instTopOfCompactSpaceOfNonempty = { top := { toCompacts := , interior_nonempty' := } }
                          Equations
                          Equations
                          • TopologicalSpace.PositiveCompacts.instOrderTopOfCompactSpaceOfNonempty = OrderTop.lift SetLike.coe
                          @[simp]

                          The image of a positive compact set under a continuous open map.

                          Equations
                          Instances For
                            @[simp]
                            theorem TopologicalSpace.PositiveCompacts.coe_map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : Continuous f) (hf' : IsOpenMap f) (s : TopologicalSpace.PositiveCompacts α) :
                            theorem exists_positiveCompacts_subset {α : Type u_1} [TopologicalSpace α] [LocallyCompactSpace α] {U : Set α} (ho : IsOpen U) (hn : U.Nonempty) :
                            theorem IsOpen.exists_positiveCompacts_closure_subset {α : Type u_1} [TopologicalSpace α] [R1Space α] [LocallyCompactSpace α] {U : Set α} (ho : IsOpen U) (hn : U.Nonempty) :
                            Equations
                            • TopologicalSpace.PositiveCompacts.instInhabitedOfCompactSpaceOfNonempty = { default := }

                            In a nonempty locally compact space, there exists a compact set with nonempty interior.

                            Equations
                            • =

                            The product of two TopologicalSpace.PositiveCompacts, as a TopologicalSpace.PositiveCompacts in the product space.

                            Equations
                            • K.prod L = { toCompacts := K.prod L.toCompacts, interior_nonempty' := }
                            Instances For

                              Compact open sets #

                              The type of compact open sets of a topological space. This is useful in non Hausdorff contexts, in particular spectral spaces.

                              Instances For
                                Equations

                                See Note [custom simps projection].

                                Equations
                                Instances For

                                  Reinterpret a compact open as an open.

                                  Equations
                                  • s.toOpens = { carrier := s, is_open' := }
                                  Instances For
                                    @[simp]

                                    Reinterpret a compact open as a clopen.

                                    Equations
                                    • s.toClopens = { carrier := s, isClopen' := }
                                    Instances For
                                      @[simp]
                                      theorem TopologicalSpace.CompactOpens.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : IsOpen s.carrier) :
                                      { toCompacts := s, isOpen' := h } = s
                                      Equations
                                      Equations
                                      • TopologicalSpace.CompactOpens.instBot = { bot := { toCompacts := , isOpen' := } }
                                      Equations
                                      Equations
                                      • TopologicalSpace.CompactOpens.instOrderBot = OrderBot.lift SetLike.coe
                                      Equations
                                      • TopologicalSpace.CompactOpens.instInhabited = { default := }
                                      Equations
                                      Equations
                                      Equations
                                      • TopologicalSpace.CompactOpens.instSDiff = { sdiff := fun (s t : TopologicalSpace.CompactOpens α) => { carrier := s \ t, isCompact' := , isOpen' := } }
                                      Equations
                                      Equations
                                      • TopologicalSpace.CompactOpens.instTop = { top := { toCompacts := , isOpen' := } }
                                      @[simp]
                                      Equations
                                      • TopologicalSpace.CompactOpens.instBoundedOrder = BoundedOrder.lift SetLike.coe
                                      Equations
                                      Equations
                                      Equations
                                      @[simp]
                                      theorem TopologicalSpace.CompactOpens.map_toCompacts {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : αβ) (hf : Continuous f) (hf' : IsOpenMap f) (s : TopologicalSpace.CompactOpens α) :
                                      (TopologicalSpace.CompactOpens.map f hf hf' s).toCompacts = TopologicalSpace.Compacts.map f hf s.toCompacts

                                      The image of a compact open under a continuous open map.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem TopologicalSpace.CompactOpens.coe_map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : Continuous f) (hf' : IsOpenMap f) (s : TopologicalSpace.CompactOpens α) :
                                        (TopologicalSpace.CompactOpens.map f hf hf' s) = f '' s
                                        theorem TopologicalSpace.CompactOpens.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : βγ) (g : αβ) (hf : Continuous f) (hg : Continuous g) (hf' : IsOpenMap f) (hg' : IsOpenMap g) (K : TopologicalSpace.CompactOpens α) :

                                        The product of two TopologicalSpace.CompactOpens, as a TopologicalSpace.CompactOpens in the product space.

                                        Equations
                                        • K.prod L = { toCompacts := K.prod L.toCompacts, isOpen' := }
                                        Instances For
                                          @[simp]