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.

Instances For

    See Note [custom simps projection].

    Instances For
      @[simp]
      theorem TopologicalSpace.Compacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : Set α) (h : IsCompact s) :
      { carrier := s, isCompact' := h } = s

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

      @[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 α} :
      ↑(Finset.sup s f) = Finset.sup s fun i => ↑(f i)

      The image of a compact set under a continuous function.

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

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

        Instances For

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

          Nonempty compact sets #

          The type of nonempty compact sets of a topological space.

          Instances For

            See Note [custom simps projection].

            Instances For

              Reinterpret a nonempty compact as a closed set.

              Instances For
                @[simp]
                theorem TopologicalSpace.NonemptyCompacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : Set.Nonempty s.carrier) :
                { toCompacts := s, nonempty' := h } = s
                @[simp]

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

                Positive compact sets #

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

                Instances For

                  See Note [custom simps projection].

                  Instances For

                    Reinterpret a positive compact as a nonempty compact.

                    Instances For
                      @[simp]
                      theorem TopologicalSpace.PositiveCompacts.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : Set.Nonempty (interior s.carrier)) :
                      { toCompacts := s, interior_nonempty' := h } = s
                      @[simp]

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

                      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 : Set.Nonempty U) :
                        K, K U

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

                        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

                          See Note [custom simps projection].

                          Instances For

                            Reinterpret a compact open as an open.

                            Instances For

                              Reinterpret a compact open as a clopen.

                              Instances For
                                @[simp]
                                theorem TopologicalSpace.CompactOpens.coe_mk {α : Type u_1} [TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : IsOpen s.carrier) :
                                { toCompacts := s, isOpen' := h } = s
                                @[simp]
                                @[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.

                                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 α) :