Documentation

Mathlib.Order.UpperLower.Principal

Principal upper/lower sets #

The results in this file all assume that the underlying type is equipped with at least a preorder.

Main declarations #

def UpperSet.Ici {α : Type u_1} [Preorder α] (a : α) :

Principal upper set. Set.Ici as an upper set. The smallest upper set containing a given element.

Equations
    Instances For
      def UpperSet.Ioi {α : Type u_1} [Preorder α] (a : α) :

      Strict principal upper set. Set.Ioi as an upper set.

      Equations
        Instances For
          @[simp]
          theorem UpperSet.coe_Ici {α : Type u_1} [Preorder α] (a : α) :
          (Ici a) = Set.Ici a
          @[simp]
          theorem UpperSet.coe_Ioi {α : Type u_1} [Preorder α] (a : α) :
          (Ioi a) = Set.Ioi a
          @[simp]
          theorem UpperSet.mem_Ici_iff {α : Type u_1} [Preorder α] {a b : α} :
          b Ici a a b
          @[simp]
          theorem UpperSet.mem_Ioi_iff {α : Type u_1} [Preorder α] {a b : α} :
          b Ioi a a < b
          @[simp]
          theorem UpperSet.map_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :
          (map f) (Ici a) = Ici (f a)
          @[simp]
          theorem UpperSet.map_Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :
          (map f) (Ioi a) = Ioi (f a)
          theorem UpperSet.Ici_le_Ioi {α : Type u_1} [Preorder α] (a : α) :
          Ici a Ioi a
          @[simp]
          theorem UpperSet.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] :
          @[simp]
          theorem UpperSet.Ioi_top {α : Type u_1} [Preorder α] [OrderTop α] :
          @[simp]
          theorem UpperSet.Ici_ne_top {α : Type u_1} [Preorder α] {a : α} :
          @[simp]
          theorem UpperSet.Ici_lt_top {α : Type u_1} [Preorder α] {a : α} :
          @[simp]
          theorem UpperSet.le_Ici {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} :
          s Ici a a s
          @[simp]
          theorem UpperSet.Ici_inj {α : Type u_1} [PartialOrder α] {a b : α} :
          Ici a = Ici b a = b
          theorem UpperSet.Ici_ne_Ici {α : Type u_1} [PartialOrder α] {a b : α} :
          Ici a Ici b a b
          @[simp]
          theorem UpperSet.Ici_sup {α : Type u_1} [SemilatticeSup α] (a b : α) :
          Ici (ab) = Ici aIci b
          @[simp]
          theorem UpperSet.Ici_sSup {α : Type u_1} [CompleteLattice α] (S : Set α) :
          Ici (sSup S) = aS, Ici a
          @[simp]
          theorem UpperSet.Ici_iSup {α : Type u_1} {ι : Sort u_3} [CompleteLattice α] (f : ια) :
          Ici (⨆ (i : ι), f i) = ⨆ (i : ι), Ici (f i)
          theorem UpperSet.Ici_iSup₂ {α : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [CompleteLattice α] (f : (i : ι) → κ iα) :
          Ici (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⨆ (i : ι), ⨆ (j : κ i), Ici (f i j)
          def LowerSet.Iic {α : Type u_1} [Preorder α] (a : α) :

          Principal lower set. Set.Iic as a lower set. The smallest lower set containing a given element.

          Equations
            Instances For
              def LowerSet.Iio {α : Type u_1} [Preorder α] (a : α) :

              Strict principal lower set. Set.Iio as a lower set.

              Equations
                Instances For
                  @[simp]
                  theorem LowerSet.coe_Iic {α : Type u_1} [Preorder α] (a : α) :
                  (Iic a) = Set.Iic a
                  @[simp]
                  theorem LowerSet.coe_Iio {α : Type u_1} [Preorder α] (a : α) :
                  (Iio a) = Set.Iio a
                  @[simp]
                  theorem LowerSet.mem_Iic_iff {α : Type u_1} [Preorder α] {a b : α} :
                  b Iic a b a
                  @[simp]
                  theorem LowerSet.mem_Iio_iff {α : Type u_1} [Preorder α] {a b : α} :
                  b Iio a b < a
                  @[simp]
                  theorem LowerSet.map_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :
                  (map f) (Iic a) = Iic (f a)
                  @[simp]
                  theorem LowerSet.map_Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :
                  (map f) (Iio a) = Iio (f a)
                  theorem LowerSet.Ioi_le_Ici {α : Type u_1} [Preorder α] (a : α) :
                  @[simp]
                  theorem LowerSet.Iic_top {α : Type u_1} [Preorder α] [OrderTop α] :
                  @[simp]
                  theorem LowerSet.Iio_bot {α : Type u_1} [Preorder α] [OrderBot α] :
                  @[simp]
                  theorem LowerSet.Iic_ne_bot {α : Type u_1} [Preorder α] {a : α} :
                  @[simp]
                  theorem LowerSet.bot_lt_Iic {α : Type u_1} [Preorder α] {a : α} :
                  @[simp]
                  theorem LowerSet.Iic_le {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} :
                  Iic a s a s
                  @[simp]
                  theorem LowerSet.Iic_inj {α : Type u_1} [PartialOrder α] {a b : α} :
                  Iic a = Iic b a = b
                  theorem LowerSet.Iic_ne_Iic {α : Type u_1} [PartialOrder α] {a b : α} :
                  Iic a Iic b a b
                  @[simp]
                  theorem LowerSet.Iic_inf {α : Type u_1} [SemilatticeInf α] (a b : α) :
                  Iic (ab) = Iic aIic b
                  @[simp]
                  theorem LowerSet.Iic_sInf {α : Type u_1} [CompleteLattice α] (S : Set α) :
                  Iic (sInf S) = aS, Iic a
                  @[simp]
                  theorem LowerSet.Iic_iInf {α : Type u_1} {ι : Sort u_3} [CompleteLattice α] (f : ια) :
                  Iic (⨅ (i : ι), f i) = ⨅ (i : ι), Iic (f i)
                  theorem LowerSet.Iic_iInf₂ {α : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [CompleteLattice α] (f : (i : ι) → κ iα) :
                  Iic (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⨅ (i : ι), ⨅ (j : κ i), Iic (f i j)