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
    theorem ClopenUpperSet.upper' {α : Type u_3} [TopologicalSpace α] [LE α] (self : ClopenUpperSet α) :
    IsUpperSet self.carrier
    Equations
    • ClopenUpperSet.instSetLike = { 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]
      theorem ClopenUpperSet.toUpperSet_coe {α : Type u_1} [TopologicalSpace α] [LE α] (s : ClopenUpperSet α) :
      s.toUpperSet = s

      Reinterpret an upper clopen as an upper set.

      Equations
      • s.toUpperSet = { carrier := s, upper' := }
      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
        instance ClopenUpperSet.instSup {α : Type u_1} [TopologicalSpace α] [LE α] :
        Equations
        • ClopenUpperSet.instSup = { sup := fun (s t : ClopenUpperSet α) => { toClopens := s.toClopens t.toClopens, upper' := } }
        instance ClopenUpperSet.instInf {α : Type u_1} [TopologicalSpace α] [LE α] :
        Equations
        • ClopenUpperSet.instInf = { inf := fun (s t : ClopenUpperSet α) => { toClopens := s.toClopens t.toClopens, upper' := } }
        instance ClopenUpperSet.instTop {α : Type u_1} [TopologicalSpace α] [LE α] :
        Equations
        • ClopenUpperSet.instTop = { top := { toClopens := , upper' := } }
        instance ClopenUpperSet.instBot {α : Type u_1} [TopologicalSpace α] [LE α] :
        Equations
        • ClopenUpperSet.instBot = { bot := { toClopens := , upper' := } }
        Equations
        Equations
        @[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.instInhabited = { default := }