Documentation

Mathlib.Topology.Sets.Order

Clopen upper sets #

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

Compact open sets #

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

The type of clopen upper sets of a topological space.

Instances For
    Equations
    • ClopenUpperSet.instSetLikeClopenUpperSet = { coe := fun (s : ClopenUpperSet α) => s.carrier, coe_injective' := }
    def ClopenUpperSet.Simps.coe {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) :
    Set α

    See Note [custom simps projection].

    Equations
    Instances For
      theorem ClopenUpperSet.upper {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) :
      theorem ClopenUpperSet.isClopen {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) :
      @[simp]

      Reinterpret an upper clopen as an upper set.

      Equations
      Instances For
        theorem ClopenUpperSet.ext {α : Type u_1} [TopologicalSpace α] [LE α] {s : ClopenUpperSet α} {t : ClopenUpperSet α} (h : s = t) :
        s = t
        @[simp]
        theorem ClopenUpperSet.coe_mk {α : Type u_1} [TopologicalSpace α] [LE α] (s : TopologicalSpace.Clopens α) (h : IsUpperSet s.carrier) :
        { toClopens := s, upper' := h } = s
        Equations
        • ClopenUpperSet.instSupClopenUpperSet = { sup := fun (s t : ClopenUpperSet α) => { toClopens := s.toClopens t.toClopens, upper' := } }
        Equations
        • ClopenUpperSet.instInfClopenUpperSet = { inf := fun (s t : ClopenUpperSet α) => { toClopens := s.toClopens t.toClopens, upper' := } }
        Equations
        • ClopenUpperSet.instTopClopenUpperSet = { top := { toClopens := , upper' := } }
        Equations
        • ClopenUpperSet.instBotClopenUpperSet = { bot := { toClopens := , upper' := } }
        Equations
        Equations
        • ClopenUpperSet.instBoundedOrderClopenUpperSetToLEToPreorderToPartialOrderToSemilatticeInfInstLatticeClopenUpperSet = BoundedOrder.lift SetLike.coe
        @[simp]
        theorem ClopenUpperSet.coe_sup {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) (t : ClopenUpperSet α) :
        (s t) = s t
        @[simp]
        theorem ClopenUpperSet.coe_inf {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) (t : ClopenUpperSet α) :
        (s t) = s t
        @[simp]
        theorem ClopenUpperSet.coe_top {α : Type u_1} [TopologicalSpace α] [LE α] :
        = Set.univ
        @[simp]
        theorem ClopenUpperSet.coe_bot {α : Type u_1} [TopologicalSpace α] [LE α] :
        =
        Equations
        • ClopenUpperSet.instInhabitedClopenUpperSet = { default := }