Documentation

Mathlib.Topology.Sets.Order

Clopen upper sets #

In this file we define the type of clopen upper sets.

Compact open sets #

source
structure ClopenUpperSet (α : Type u_2) [TopologicalSpace α] [LE α] extends TopologicalSpace.Clopens α :
Type u_2

The type of clopen upper sets of a topological space.

Instances For
    source
    instance ClopenUpperSet.instSetLike {α : Type u_1} [TopologicalSpace α] [LE α] :
    SetLike (ClopenUpperSet α) α
    Equations
      source
      def ClopenUpperSet.Simps.coe {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) :
      Set α

      See Note [custom simps projection].

      Equations
        Instances For
          source
          theorem ClopenUpperSet.upper {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) :
          IsUpperSet ↑s
          source
          theorem ClopenUpperSet.isClopen {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) :
          IsClopen ↑s
          source
          def ClopenUpperSet.toUpperSet {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) :
          UpperSet α

          Reinterpret an upper clopen as an upper set.

          Equations
            Instances For
              source
              @[simp]
              theorem ClopenUpperSet.coe_toUpperSet {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) :
              ↑s.toUpperSet = ↑s
              source
              theorem ClopenUpperSet.ext {α : Type u_1} [TopologicalSpace α] [LE α] {s t : ClopenUpperSet α} (h : ↑s = ↑t) :
              s = t
              source
              theorem ClopenUpperSet.ext_iff {α : Type u_1} [TopologicalSpace α] [LE α] {s t : ClopenUpperSet α} :
              s = t ↔ ↑s = ↑t
              source
              @[simp]
              theorem ClopenUpperSet.coe_mk {α : Type u_1} [TopologicalSpace α] [LE α] (s : TopologicalSpace.Clopens α) (h : IsUpperSet s.carrier) :
              ↑{ toClopens := s, upper' := h } = ↑s
              source
              instance ClopenUpperSet.instMax {α : Type u_1} [TopologicalSpace α] [LE α] :
              Max (ClopenUpperSet α)
              Equations
                source
                instance ClopenUpperSet.instMin {α : Type u_1} [TopologicalSpace α] [LE α] :
                Min (ClopenUpperSet α)
                Equations
                  source
                  instance ClopenUpperSet.instTop {α : Type u_1} [TopologicalSpace α] [LE α] :
                  Top (ClopenUpperSet α)
                  Equations
                    source
                    instance ClopenUpperSet.instBot {α : Type u_1} [TopologicalSpace α] [LE α] :
                    Bot (ClopenUpperSet α)
                    Equations
                      source
                      instance ClopenUpperSet.instLattice {α : Type u_1} [TopologicalSpace α] [LE α] :
                      Lattice (ClopenUpperSet α)
                      Equations
                        source
                        instance ClopenUpperSet.instBoundedOrder {α : Type u_1} [TopologicalSpace α] [LE α] :
                        BoundedOrder (ClopenUpperSet α)
                        Equations
                          source
                          @[simp]
                          theorem ClopenUpperSet.coe_sup {α : Type u_1} [TopologicalSpace α] [LE α] (s t : ClopenUpperSet α) :
                          ↑(s ⊔ t) = ↑s ∪ ↑t
                          source
                          @[simp]
                          theorem ClopenUpperSet.coe_inf {α : Type u_1} [TopologicalSpace α] [LE α] (s t : ClopenUpperSet α) :
                          ↑(s ⊓ t) = ↑s ∩ ↑t
                          source
                          @[simp]
                          theorem ClopenUpperSet.coe_top {α : Type u_1} [TopologicalSpace α] [LE α] :
                          ↑⊤ = Set.univ
                          source
                          @[simp]
                          theorem ClopenUpperSet.coe_bot {α : Type u_1} [TopologicalSpace α] [LE α] :
                          ↑⊥ = ∅
                          source
                          instance ClopenUpperSet.instInhabited {α : Type u_1} [TopologicalSpace α] [LE α] :
                          Inhabited (ClopenUpperSet α)
                          Equations