Documentation

Mathlib.Order.Bounds.Basic

Upper / lower bounds #

In this file we define:

Definitions #

def upperBounds {α : Type u} [Preorder α] (s : Set α) :
Set α

The set of upper bounds of a set.

Equations
Instances For
    def lowerBounds {α : Type u} [Preorder α] (s : Set α) :
    Set α

    The set of lower bounds of a set.

    Equations
    Instances For
      def BddAbove {α : Type u} [Preorder α] (s : Set α) :

      A set is bounded above if there exists an upper bound.

      Equations
      Instances For
        def BddBelow {α : Type u} [Preorder α] (s : Set α) :

        A set is bounded below if there exists a lower bound.

        Equations
        Instances For
          def IsLeast {α : Type u} [Preorder α] (s : Set α) (a : α) :

          a is a least element of a set s; for a partial order, it is unique if exists.

          Equations
          Instances For
            def IsGreatest {α : Type u} [Preorder α] (s : Set α) (a : α) :

            a is a greatest element of a set s; for a partial order, it is unique if exists.

            Equations
            Instances For
              def IsLUB {α : Type u} [Preorder α] (s : Set α) :
              αProp

              a is a least upper bound of a set s; for a partial order, it is unique if exists.

              Equations
              Instances For
                def IsGLB {α : Type u} [Preorder α] (s : Set α) :
                αProp

                a is a greatest lower bound of a set s; for a partial order, it is unique if exists.

                Equations
                Instances For
                  theorem mem_upperBounds {α : Type u} [Preorder α] {s : Set α} {a : α} :
                  a upperBounds s xs, x a
                  theorem mem_lowerBounds {α : Type u} [Preorder α] {s : Set α} {a : α} :
                  a lowerBounds s xs, a x
                  theorem mem_upperBounds_iff_subset_Iic {α : Type u} [Preorder α] {s : Set α} {a : α} :
                  theorem mem_lowerBounds_iff_subset_Ici {α : Type u} [Preorder α] {s : Set α} {a : α} :
                  theorem bddAbove_def {α : Type u} [Preorder α] {s : Set α} :
                  BddAbove s ∃ (x : α), ys, y x
                  theorem bddBelow_def {α : Type u} [Preorder α] {s : Set α} :
                  BddBelow s ∃ (x : α), ys, x y
                  theorem bot_mem_lowerBounds {α : Type u} [Preorder α] [OrderBot α] (s : Set α) :
                  theorem top_mem_upperBounds {α : Type u} [Preorder α] [OrderTop α] (s : Set α) :
                  @[simp]
                  theorem isLeast_bot_iff {α : Type u} [Preorder α] {s : Set α} [OrderBot α] :
                  @[simp]
                  theorem isGreatest_top_iff {α : Type u} [Preorder α] {s : Set α} [OrderTop α] :
                  theorem not_bddAbove_iff' {α : Type u} [Preorder α] {s : Set α} :
                  ¬BddAbove s ∀ (x : α), ys, ¬y x

                  A set s is not bounded above if and only if for each x there exists y ∈ s such that x is not greater than or equal to y. This version only assumes Preorder structure and uses ¬(y ≤ x). A version for linear orders is called not_bddAbove_iff.

                  theorem not_bddBelow_iff' {α : Type u} [Preorder α] {s : Set α} :
                  ¬BddBelow s ∀ (x : α), ys, ¬x y

                  A set s is not bounded below if and only if for each x there exists y ∈ s such that x is not less than or equal to y. This version only assumes Preorder structure and uses ¬(x ≤ y). A version for linear orders is called not_bddBelow_iff.

                  theorem not_bddAbove_iff {α : Type u_1} [LinearOrder α] {s : Set α} :
                  ¬BddAbove s ∀ (x : α), ys, x < y

                  A set s is not bounded above if and only if for each x there exists y ∈ s that is greater than x. A version for preorders is called not_bddAbove_iff'.

                  theorem not_bddBelow_iff {α : Type u_1} [LinearOrder α] {s : Set α} :
                  ¬BddBelow s ∀ (x : α), ys, y < x

                  A set s is not bounded below if and only if for each x there exists y ∈ s that is less than x. A version for preorders is called not_bddBelow_iff'.

                  @[simp]
                  theorem bddBelow_preimage_ofDual {α : Type u} [Preorder α] {s : Set α} :
                  BddBelow (OrderDual.ofDual ⁻¹' s) BddAbove s
                  @[simp]
                  theorem bddAbove_preimage_ofDual {α : Type u} [Preorder α] {s : Set α} :
                  BddAbove (OrderDual.ofDual ⁻¹' s) BddBelow s
                  @[simp]
                  theorem bddBelow_preimage_toDual {α : Type u} [Preorder α] {s : Set αᵒᵈ} :
                  BddBelow (OrderDual.toDual ⁻¹' s) BddAbove s
                  @[simp]
                  theorem bddAbove_preimage_toDual {α : Type u} [Preorder α] {s : Set αᵒᵈ} :
                  BddAbove (OrderDual.toDual ⁻¹' s) BddBelow s
                  theorem BddAbove.dual {α : Type u} [Preorder α] {s : Set α} (h : BddAbove s) :
                  BddBelow (OrderDual.ofDual ⁻¹' s)
                  theorem BddBelow.dual {α : Type u} [Preorder α] {s : Set α} (h : BddBelow s) :
                  BddAbove (OrderDual.ofDual ⁻¹' s)
                  theorem IsLeast.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) :
                  IsGreatest (OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
                  theorem IsGreatest.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) :
                  IsLeast (OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
                  theorem IsLUB.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) :
                  IsGLB (OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
                  theorem IsGLB.dual {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) :
                  IsLUB (OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
                  @[reducible, inline]
                  abbrev IsLeast.orderBot {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) :

                  If a is the least element of a set s, then subtype s is an order with bottom element.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev IsGreatest.orderTop {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) :

                    If a is the greatest element of a set s, then subtype s is an order with top element.

                    Equations
                    Instances For

                      Monotonicity #

                      theorem upperBounds_mono_set {α : Type u} [Preorder α] ⦃s : Set α ⦃t : Set α (hst : s t) :
                      theorem lowerBounds_mono_set {α : Type u} [Preorder α] ⦃s : Set α ⦃t : Set α (hst : s t) :
                      theorem upperBounds_mono_mem {α : Type u} [Preorder α] {s : Set α} ⦃a : α ⦃b : α (hab : a b) :
                      theorem lowerBounds_mono_mem {α : Type u} [Preorder α] {s : Set α} ⦃a : α ⦃b : α (hab : a b) :
                      theorem upperBounds_mono {α : Type u} [Preorder α] ⦃s : Set α ⦃t : Set α (hst : s t) ⦃a : α ⦃b : α (hab : a b) :
                      theorem lowerBounds_mono {α : Type u} [Preorder α] ⦃s : Set α ⦃t : Set α (hst : s t) ⦃a : α ⦃b : α (hab : a b) :
                      theorem BddAbove.mono {α : Type u} [Preorder α] ⦃s : Set α ⦃t : Set α (h : s t) :

                      If s ⊆ t and t is bounded above, then so is s.

                      theorem BddBelow.mono {α : Type u} [Preorder α] ⦃s : Set α ⦃t : Set α (h : s t) :

                      If s ⊆ t and t is bounded below, then so is s.

                      theorem IsLUB.of_subset_of_superset {α : Type u} [Preorder α] {a : α} {s : Set α} {t : Set α} {p : Set α} (hs : IsLUB s a) (hp : IsLUB p a) (hst : s t) (htp : t p) :
                      IsLUB t a

                      If a is a least upper bound for sets s and p, then it is a least upper bound for any set t, s ⊆ t ⊆ p.

                      theorem IsGLB.of_subset_of_superset {α : Type u} [Preorder α] {a : α} {s : Set α} {t : Set α} {p : Set α} (hs : IsGLB s a) (hp : IsGLB p a) (hst : s t) (htp : t p) :
                      IsGLB t a

                      If a is a greatest lower bound for sets s and p, then it is a greater lower bound for any set t, s ⊆ t ⊆ p.

                      theorem IsLeast.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsLeast s a) (hb : IsLeast t b) (hst : s t) :
                      b a
                      theorem IsGreatest.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsGreatest s a) (hb : IsGreatest t b) (hst : s t) :
                      a b
                      theorem IsLUB.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsLUB s a) (hb : IsLUB t b) (hst : s t) :
                      a b
                      theorem IsGLB.mono {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} {b : α} (ha : IsGLB s a) (hb : IsGLB t b) (hst : s t) :
                      b a
                      theorem Set.Nonempty.bddAbove_lowerBounds {α : Type u} [Preorder α] {s : Set α} (hs : s.Nonempty) :
                      theorem Set.Nonempty.bddBelow_upperBounds {α : Type u} [Preorder α] {s : Set α} (hs : s.Nonempty) :

                      Conversions #

                      theorem IsLeast.isGLB {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) :
                      IsGLB s a
                      theorem IsGreatest.isLUB {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) :
                      IsLUB s a
                      theorem IsLUB.upperBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) :
                      theorem IsGLB.lowerBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) :
                      theorem IsLeast.lowerBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) :
                      theorem IsGreatest.upperBounds_eq {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) :
                      theorem IsGreatest.lt_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsGreatest s a) :
                      a < b xs, x < b
                      theorem IsLeast.lt_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsLeast s a) :
                      b < a xs, b < x
                      theorem isLUB_le_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) :
                      theorem le_isGLB_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) :
                      theorem isLUB_iff_le_iff {α : Type u} [Preorder α] {s : Set α} {a : α} :
                      IsLUB s a ∀ (b : α), a b b upperBounds s
                      theorem isGLB_iff_le_iff {α : Type u} [Preorder α] {s : Set α} {a : α} :
                      IsGLB s a ∀ (b : α), b a b lowerBounds s
                      theorem IsLUB.bddAbove {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) :

                      If s has a least upper bound, then it is bounded above.

                      theorem IsGLB.bddBelow {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) :

                      If s has a greatest lower bound, then it is bounded below.

                      theorem IsGreatest.bddAbove {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) :

                      If s has a greatest element, then it is bounded above.

                      theorem IsLeast.bddBelow {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) :

                      If s has a least element, then it is bounded below.

                      theorem IsLeast.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) :
                      s.Nonempty
                      theorem IsGreatest.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) :
                      s.Nonempty

                      Union and intersection #

                      @[simp]
                      theorem upperBounds_union {α : Type u} [Preorder α] {s : Set α} {t : Set α} :
                      @[simp]
                      theorem lowerBounds_union {α : Type u} [Preorder α] {s : Set α} {t : Set α} :
                      theorem isLeast_union_iff {α : Type u} [Preorder α] {a : α} {s : Set α} {t : Set α} :
                      theorem isGreatest_union_iff {α : Type u} [Preorder α] {s : Set α} {t : Set α} {a : α} :
                      theorem BddAbove.inter_of_left {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddAbove s) :

                      If s is bounded, then so is s ∩ t

                      theorem BddAbove.inter_of_right {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddAbove t) :

                      If t is bounded, then so is s ∩ t

                      theorem BddBelow.inter_of_left {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddBelow s) :

                      If s is bounded, then so is s ∩ t

                      theorem BddBelow.inter_of_right {α : Type u} [Preorder α] {s : Set α} {t : Set α} (h : BddBelow t) :

                      If t is bounded, then so is s ∩ t

                      theorem BddAbove.union {α : Type u} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} :
                      BddAbove sBddAbove tBddAbove (s t)

                      In a directed order, the union of bounded above sets is bounded above.

                      theorem bddAbove_union {α : Type u} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} :

                      In a directed order, the union of two sets is bounded above if and only if both sets are.

                      theorem BddBelow.union {α : Type u} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} :
                      BddBelow sBddBelow tBddBelow (s t)

                      In a codirected order, the union of bounded below sets is bounded below.

                      theorem bddBelow_union {α : Type u} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] {s : Set α} {t : Set α} :

                      In a codirected order, the union of two sets is bounded below if and only if both sets are.

                      theorem IsLUB.union {γ : Type w} [SemilatticeSup γ] {a : γ} {b : γ} {s : Set γ} {t : Set γ} (hs : IsLUB s a) (ht : IsLUB t b) :
                      IsLUB (s t) (a b)

                      If a is the least upper bound of s and b is the least upper bound of t, then a ⊔ b is the least upper bound of s ∪ t.

                      theorem IsGLB.union {γ : Type w} [SemilatticeInf γ] {a₁ : γ} {a₂ : γ} {s : Set γ} {t : Set γ} (hs : IsGLB s a₁) (ht : IsGLB t a₂) :
                      IsGLB (s t) (a₁ a₂)

                      If a is the greatest lower bound of s and b is the greatest lower bound of t, then a ⊓ b is the greatest lower bound of s ∪ t.

                      theorem IsLeast.union {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} {s : Set γ} {t : Set γ} (ha : IsLeast s a) (hb : IsLeast t b) :
                      IsLeast (s t) (min a b)

                      If a is the least element of s and b is the least element of t, then min a b is the least element of s ∪ t.

                      theorem IsGreatest.union {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} {s : Set γ} {t : Set γ} (ha : IsGreatest s a) (hb : IsGreatest t b) :
                      IsGreatest (s t) (max a b)

                      If a is the greatest element of s and b is the greatest element of t, then max a b is the greatest element of s ∪ t.

                      theorem IsLUB.inter_Ici_of_mem {γ : Type w} [LinearOrder γ] {s : Set γ} {a : γ} {b : γ} (ha : IsLUB s a) (hb : b s) :
                      IsLUB (s Set.Ici b) a
                      theorem IsGLB.inter_Iic_of_mem {γ : Type w} [LinearOrder γ] {s : Set γ} {a : γ} {b : γ} (ha : IsGLB s a) (hb : b s) :
                      IsGLB (s Set.Iic b) a
                      theorem bddAbove_iff_exists_ge {γ : Type w} [SemilatticeSup γ] {s : Set γ} (x₀ : γ) :
                      BddAbove s ∃ (x : γ), x₀ x ys, y x
                      theorem bddBelow_iff_exists_le {γ : Type w} [SemilatticeInf γ] {s : Set γ} (x₀ : γ) :
                      BddBelow s xx₀, ys, x y
                      theorem BddAbove.exists_ge {γ : Type w} [SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x₀ : γ) :
                      ∃ (x : γ), x₀ x ys, y x
                      theorem BddBelow.exists_le {γ : Type w} [SemilatticeInf γ] {s : Set γ} (hs : BddBelow s) (x₀ : γ) :
                      xx₀, ys, x y

                      Specific sets #

                      Unbounded intervals #

                      theorem isLeast_Ici {α : Type u} [Preorder α] {a : α} :
                      theorem isGreatest_Iic {α : Type u} [Preorder α] {a : α} :
                      theorem isLUB_Iic {α : Type u} [Preorder α] {a : α} :
                      theorem isGLB_Ici {α : Type u} [Preorder α] {a : α} :
                      theorem upperBounds_Iic {α : Type u} [Preorder α] {a : α} :
                      theorem lowerBounds_Ici {α : Type u} [Preorder α] {a : α} :
                      theorem bddAbove_Iic {α : Type u} [Preorder α] {a : α} :
                      theorem bddBelow_Ici {α : Type u} [Preorder α] {a : α} :
                      theorem bddAbove_Iio {α : Type u} [Preorder α] {a : α} :
                      theorem bddBelow_Ioi {α : Type u} [Preorder α] {a : α} :
                      theorem lub_Iio_le {α : Type u} [Preorder α] {b : α} (a : α) (hb : IsLUB (Set.Iio a) b) :
                      b a
                      theorem le_glb_Ioi {α : Type u} [Preorder α] {b : α} (a : α) (hb : IsGLB (Set.Ioi a) b) :
                      a b
                      theorem lub_Iio_eq_self_or_Iio_eq_Iic {γ : Type w} [PartialOrder γ] {j : γ} (i : γ) (hj : IsLUB (Set.Iio i) j) :
                      theorem glb_Ioi_eq_self_or_Ioi_eq_Ici {γ : Type w} [PartialOrder γ] {j : γ} (i : γ) (hj : IsGLB (Set.Ioi i) j) :
                      theorem exists_lub_Iio {γ : Type w} [LinearOrder γ] (i : γ) :
                      ∃ (j : γ), IsLUB (Set.Iio i) j
                      theorem exists_glb_Ioi {γ : Type w} [LinearOrder γ] (i : γ) :
                      ∃ (j : γ), IsGLB (Set.Ioi i) j
                      theorem isLUB_Iio {γ : Type w} [LinearOrder γ] [DenselyOrdered γ] {a : γ} :
                      theorem isGLB_Ioi {γ : Type w} [LinearOrder γ] [DenselyOrdered γ] {a : γ} :

                      Singleton #

                      @[simp]
                      theorem isGreatest_singleton {α : Type u} [Preorder α] {a : α} :
                      @[simp]
                      theorem isLeast_singleton {α : Type u} [Preorder α] {a : α} :
                      IsLeast {a} a
                      @[simp]
                      theorem isLUB_singleton {α : Type u} [Preorder α] {a : α} :
                      IsLUB {a} a
                      @[simp]
                      theorem isGLB_singleton {α : Type u} [Preorder α] {a : α} :
                      IsGLB {a} a
                      @[simp]
                      theorem bddAbove_singleton {α : Type u} [Preorder α] {a : α} :
                      @[simp]
                      theorem bddBelow_singleton {α : Type u} [Preorder α] {a : α} :
                      @[simp]
                      theorem upperBounds_singleton {α : Type u} [Preorder α] {a : α} :
                      @[simp]
                      theorem lowerBounds_singleton {α : Type u} [Preorder α] {a : α} :

                      Bounded intervals #

                      theorem bddAbove_Icc {α : Type u} [Preorder α] {a : α} {b : α} :
                      theorem bddBelow_Icc {α : Type u} [Preorder α] {a : α} {b : α} :
                      theorem bddAbove_Ico {α : Type u} [Preorder α] {a : α} {b : α} :
                      theorem bddBelow_Ico {α : Type u} [Preorder α] {a : α} {b : α} :
                      theorem bddAbove_Ioc {α : Type u} [Preorder α] {a : α} {b : α} :
                      theorem bddBelow_Ioc {α : Type u} [Preorder α] {a : α} {b : α} :
                      theorem bddAbove_Ioo {α : Type u} [Preorder α] {a : α} {b : α} :
                      theorem bddBelow_Ioo {α : Type u} [Preorder α] {a : α} {b : α} :
                      theorem isGreatest_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a b) :
                      theorem isLUB_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a b) :
                      IsLUB (Set.Icc a b) b
                      theorem upperBounds_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a b) :
                      theorem isLeast_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a b) :
                      theorem isGLB_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a b) :
                      IsGLB (Set.Icc a b) a
                      theorem lowerBounds_Icc {α : Type u} [Preorder α] {a : α} {b : α} (h : a b) :
                      theorem isGreatest_Ioc {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) :
                      theorem isLUB_Ioc {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) :
                      IsLUB (Set.Ioc a b) b
                      theorem upperBounds_Ioc {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) :
                      theorem isLeast_Ico {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) :
                      theorem isGLB_Ico {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) :
                      IsGLB (Set.Ico a b) a
                      theorem lowerBounds_Ico {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) :
                      theorem isGLB_Ioo {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (h : a < b) :
                      IsGLB (Set.Ioo a b) a
                      theorem lowerBounds_Ioo {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :
                      theorem isGLB_Ioc {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :
                      IsGLB (Set.Ioc a b) a
                      theorem lowerBounds_Ioc {γ : Type w} [SemilatticeSup γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :
                      theorem isLUB_Ioo {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :
                      IsLUB (Set.Ioo a b) b
                      theorem upperBounds_Ioo {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :
                      theorem isLUB_Ico {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :
                      IsLUB (Set.Ico a b) b
                      theorem upperBounds_Ico {γ : Type w} [SemilatticeInf γ] [DenselyOrdered γ] {a : γ} {b : γ} (hab : a < b) :
                      theorem bddBelow_iff_subset_Ici {α : Type u} [Preorder α] {s : Set α} :
                      BddBelow s ∃ (a : α), s Set.Ici a
                      theorem bddAbove_iff_subset_Iic {α : Type u} [Preorder α] {s : Set α} :
                      BddAbove s ∃ (a : α), s Set.Iic a
                      theorem bddBelow_bddAbove_iff_subset_Icc {α : Type u} [Preorder α] {s : Set α} :
                      BddBelow s BddAbove s ∃ (a : α) (b : α), s Set.Icc a b

                      Univ #

                      @[simp]
                      theorem isGreatest_univ_iff {α : Type u} [Preorder α] {a : α} :
                      IsGreatest Set.univ a IsTop a
                      theorem isGreatest_univ {α : Type u} [Preorder α] [OrderTop α] :
                      IsGreatest Set.univ
                      @[simp]
                      theorem OrderTop.upperBounds_univ {γ : Type w} [PartialOrder γ] [OrderTop γ] :
                      upperBounds Set.univ = {}
                      theorem isLUB_univ {α : Type u} [Preorder α] [OrderTop α] :
                      IsLUB Set.univ
                      @[simp]
                      theorem OrderBot.lowerBounds_univ {γ : Type w} [PartialOrder γ] [OrderBot γ] :
                      lowerBounds Set.univ = {}
                      @[simp]
                      theorem isLeast_univ_iff {α : Type u} [Preorder α] {a : α} :
                      IsLeast Set.univ a IsBot a
                      theorem isLeast_univ {α : Type u} [Preorder α] [OrderBot α] :
                      IsLeast Set.univ
                      theorem isGLB_univ {α : Type u} [Preorder α] [OrderBot α] :
                      IsGLB Set.univ
                      @[simp]
                      theorem NoMaxOrder.upperBounds_univ {α : Type u} [Preorder α] [NoMaxOrder α] :
                      upperBounds Set.univ =
                      @[simp]
                      theorem NoMinOrder.lowerBounds_univ {α : Type u} [Preorder α] [NoMinOrder α] :
                      lowerBounds Set.univ =
                      @[simp]
                      theorem not_bddAbove_univ {α : Type u} [Preorder α] [NoMaxOrder α] :
                      ¬BddAbove Set.univ
                      @[simp]
                      theorem not_bddBelow_univ {α : Type u} [Preorder α] [NoMinOrder α] :
                      ¬BddBelow Set.univ

                      Empty set #

                      @[simp]
                      theorem upperBounds_empty {α : Type u} [Preorder α] :
                      upperBounds = Set.univ
                      @[simp]
                      theorem lowerBounds_empty {α : Type u} [Preorder α] :
                      lowerBounds = Set.univ
                      @[simp]
                      theorem bddAbove_empty {α : Type u} [Preorder α] [Nonempty α] :
                      @[simp]
                      theorem bddBelow_empty {α : Type u} [Preorder α] [Nonempty α] :
                      @[simp]
                      theorem isGLB_empty_iff {α : Type u} [Preorder α] {a : α} :
                      @[simp]
                      theorem isLUB_empty_iff {α : Type u} [Preorder α] {a : α} :
                      theorem isGLB_empty {α : Type u} [Preorder α] [OrderTop α] :
                      theorem isLUB_empty {α : Type u} [Preorder α] [OrderBot α] :
                      theorem IsLUB.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} [NoMinOrder α] (hs : IsLUB s a) :
                      s.Nonempty
                      theorem IsGLB.nonempty {α : Type u} [Preorder α] {s : Set α} {a : α} [NoMaxOrder α] (hs : IsGLB s a) :
                      s.Nonempty
                      theorem nonempty_of_not_bddAbove {α : Type u} [Preorder α] {s : Set α} [ha : Nonempty α] (h : ¬BddAbove s) :
                      s.Nonempty
                      theorem nonempty_of_not_bddBelow {α : Type u} [Preorder α] {s : Set α} [Nonempty α] (h : ¬BddBelow s) :
                      s.Nonempty

                      insert #

                      @[simp]
                      theorem bddAbove_insert {α : Type u} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] {s : Set α} {a : α} :

                      Adding a point to a set preserves its boundedness above.

                      theorem BddAbove.insert {α : Type u} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] {s : Set α} (a : α) :
                      @[simp]
                      theorem bddBelow_insert {α : Type u} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] {s : Set α} {a : α} :

                      Adding a point to a set preserves its boundedness below.

                      theorem BddBelow.insert {α : Type u} [Preorder α] [IsDirected α fun (x x_1 : α) => x x_1] {s : Set α} (a : α) :
                      theorem IsLUB.insert {γ : Type w} [SemilatticeSup γ] (a : γ) {b : γ} {s : Set γ} (hs : IsLUB s b) :
                      IsLUB (insert a s) (a b)
                      theorem IsGLB.insert {γ : Type w} [SemilatticeInf γ] (a : γ) {b : γ} {s : Set γ} (hs : IsGLB s b) :
                      IsGLB (insert a s) (a b)
                      theorem IsGreatest.insert {γ : Type w} [LinearOrder γ] (a : γ) {b : γ} {s : Set γ} (hs : IsGreatest s b) :
                      IsGreatest (insert a s) (max a b)
                      theorem IsLeast.insert {γ : Type w} [LinearOrder γ] (a : γ) {b : γ} {s : Set γ} (hs : IsLeast s b) :
                      IsLeast (insert a s) (min a b)
                      @[simp]
                      theorem upperBounds_insert {α : Type u} [Preorder α] (a : α) (s : Set α) :
                      @[simp]
                      theorem lowerBounds_insert {α : Type u} [Preorder α] (a : α) (s : Set α) :
                      @[simp]
                      theorem OrderTop.bddAbove {α : Type u} [Preorder α] [OrderTop α] (s : Set α) :

                      When there is a global maximum, every set is bounded above.

                      @[simp]
                      theorem OrderBot.bddBelow {α : Type u} [Preorder α] [OrderBot α] (s : Set α) :

                      When there is a global minimum, every set is bounded below.

                      Sets are automatically bounded or cobounded in complete lattices. To use the same statements in complete and conditionally complete lattices but let automation fill automatically the boundedness proofs in complete lattices, we use the tactic bddDefault in the statements, in the form (hA : BddAbove A := by bddDefault).

                      Equations
                      Instances For

                        Pair #

                        theorem isLUB_pair {γ : Type w} [SemilatticeSup γ] {a : γ} {b : γ} :
                        IsLUB {a, b} (a b)
                        theorem isGLB_pair {γ : Type w} [SemilatticeInf γ] {a : γ} {b : γ} :
                        IsGLB {a, b} (a b)
                        theorem isLeast_pair {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} :
                        IsLeast {a, b} (min a b)
                        theorem isGreatest_pair {γ : Type w} [LinearOrder γ] {a : γ} {b : γ} :
                        IsGreatest {a, b} (max a b)

                        Lower/upper bounds #

                        @[simp]
                        theorem isLUB_lowerBounds {α : Type u} [Preorder α] {s : Set α} {a : α} :
                        @[simp]
                        theorem isGLB_upperBounds {α : Type u} [Preorder α] {s : Set α} {a : α} :

                        (In)equalities with the least upper bound and the greatest lower bound #

                        theorem lowerBounds_le_upperBounds {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : a lowerBounds s) (hb : b upperBounds s) :
                        s.Nonemptya b
                        theorem isGLB_le_isLUB {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : IsGLB s a) (hb : IsLUB s b) (hs : s.Nonempty) :
                        a b
                        theorem isLUB_lt_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : IsLUB s a) :
                        a < b cupperBounds s, c < b
                        theorem lt_isGLB_iff {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} (ha : IsGLB s a) :
                        b < a clowerBounds s, b < c
                        theorem le_of_isLUB_le_isGLB {α : Type u} [Preorder α] {s : Set α} {a : α} {b : α} {x : α} {y : α} (ha : IsGLB s a) (hb : IsLUB s b) (hab : b a) (hx : x s) (hy : y s) :
                        x y
                        theorem IsLeast.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsLeast s a) (Hb : IsLeast s b) :
                        a = b
                        theorem IsLeast.isLeast_iff_eq {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsLeast s a) :
                        IsLeast s b a = b
                        theorem IsGreatest.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGreatest s a) (Hb : IsGreatest s b) :
                        a = b
                        theorem IsGreatest.isGreatest_iff_eq {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGreatest s a) :
                        IsGreatest s b a = b
                        theorem IsLUB.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsLUB s a) (Hb : IsLUB s b) :
                        a = b
                        theorem IsGLB.unique {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGLB s a) (Hb : IsGLB s b) :
                        a = b
                        theorem Set.subsingleton_of_isLUB_le_isGLB {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGLB s a) (Hb : IsLUB s b) (hab : b a) :
                        s.Subsingleton
                        theorem isGLB_lt_isLUB_of_ne {α : Type u} [PartialOrder α] {s : Set α} {a : α} {b : α} (Ha : IsGLB s a) (Hb : IsLUB s b) {x : α} {y : α} (Hx : x s) (Hy : y s) (Hxy : x y) :
                        a < b
                        theorem lt_isLUB_iff {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) :
                        b < a cs, b < c
                        theorem isGLB_lt_iff {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) :
                        a < b cs, c < b
                        theorem IsLUB.exists_between {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) (hb : b < a) :
                        cs, b < c c a
                        theorem IsLUB.exists_between' {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsLUB s a) (h' : as) (hb : b < a) :
                        cs, b < c c < a
                        theorem IsGLB.exists_between {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) (hb : a < b) :
                        cs, a c c < b
                        theorem IsGLB.exists_between' {α : Type u} [LinearOrder α] {s : Set α} {a : α} {b : α} (h : IsGLB s a) (h' : as) (hb : a < b) :
                        cs, a < c c < b

                        Images of upper/lower bounds under monotone functions #

                        theorem MonotoneOn.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) {a : α} (Hst : s t) (Has : a upperBounds s) (Hat : a t) :
                        f a upperBounds (f '' s)
                        theorem MonotoneOn.mem_upperBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {t : Set α} (Hf : MonotoneOn f t) {a : α} :
                        a upperBounds ta tf a upperBounds (f '' t)
                        theorem MonotoneOn.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) {a : α} (Hst : s t) (Has : a lowerBounds s) (Hat : a t) :
                        f a lowerBounds (f '' s)
                        theorem MonotoneOn.mem_lowerBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {t : Set α} (Hf : MonotoneOn f t) {a : α} :
                        a lowerBounds ta tf a lowerBounds (f '' t)
                        theorem MonotoneOn.image_upperBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) (Hst : s t) :
                        theorem MonotoneOn.image_lowerBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) (Hst : s t) :
                        theorem MonotoneOn.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) (Hst : s t) :
                        (upperBounds s t).NonemptyBddAbove (f '' s)

                        The image under a monotone function on a set t of a subset which has an upper bound in t is bounded above.

                        theorem MonotoneOn.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : MonotoneOn f t) (Hst : s t) :
                        (lowerBounds s t).NonemptyBddBelow (f '' s)

                        The image under a monotone function on a set t of a subset which has a lower bound in t is bounded below.

                        theorem MonotoneOn.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {t : Set α} (Hf : MonotoneOn f t) {a : α} (Ha : IsLeast t a) :
                        IsLeast (f '' t) (f a)

                        A monotone map sends a least element of a set to a least element of its image.

                        theorem MonotoneOn.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {t : Set α} (Hf : MonotoneOn f t) {a : α} (Ha : IsGreatest t a) :
                        IsGreatest (f '' t) (f a)

                        A monotone map sends a greatest element of a set to a greatest element of its image.

                        theorem AntitoneOn.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) {a : α} (Hst : s t) (Has : a lowerBounds s) :
                        a tf a upperBounds (f '' s)
                        theorem AntitoneOn.mem_upperBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {t : Set α} (Hf : AntitoneOn f t) {a : α} :
                        a lowerBounds ta tf a upperBounds (f '' t)
                        theorem AntitoneOn.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) {a : α} (Hst : s t) :
                        a upperBounds sa tf a lowerBounds (f '' s)
                        theorem AntitoneOn.mem_lowerBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {t : Set α} (Hf : AntitoneOn f t) {a : α} :
                        a upperBounds ta tf a lowerBounds (f '' t)
                        theorem AntitoneOn.image_lowerBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) (Hst : s t) :
                        theorem AntitoneOn.image_upperBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) (Hst : s t) :
                        theorem AntitoneOn.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) (Hst : s t) :
                        (upperBounds s t).NonemptyBddBelow (f '' s)

                        The image under an antitone function of a set which is bounded above is bounded below.

                        theorem AntitoneOn.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {t : Set α} (Hf : AntitoneOn f t) (Hst : s t) :
                        (lowerBounds s t).NonemptyBddAbove (f '' s)

                        The image under an antitone function of a set which is bounded below is bounded above.

                        theorem AntitoneOn.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {t : Set α} (Hf : AntitoneOn f t) {a : α} :
                        IsGreatest t aIsLeast (f '' t) (f a)

                        An antitone map sends a greatest element of a set to a least element of its image.

                        theorem AntitoneOn.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {t : Set α} (Hf : AntitoneOn f t) {a : α} :
                        IsLeast t aIsGreatest (f '' t) (f a)

                        An antitone map sends a least element of a set to a greatest element of its image.

                        theorem Monotone.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (Hf : Monotone f) {a : α} {s : Set α} (Ha : a upperBounds s) :
                        f a upperBounds (f '' s)
                        theorem Monotone.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (Hf : Monotone f) {a : α} {s : Set α} (Ha : a lowerBounds s) :
                        f a lowerBounds (f '' s)
                        theorem Monotone.image_upperBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} {s : Set α} (Hf : Monotone f) :
                        theorem Monotone.image_lowerBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (Hf : Monotone f) {s : Set α} :
                        theorem Monotone.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (Hf : Monotone f) {s : Set α} :
                        BddAbove sBddAbove (f '' s)

                        The image under a monotone function of a set which is bounded above is bounded above. See also BddAbove.image2.

                        theorem Monotone.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (Hf : Monotone f) {s : Set α} :
                        BddBelow sBddBelow (f '' s)

                        The image under a monotone function of a set which is bounded below is bounded below. See also BddBelow.image2.

                        theorem Monotone.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (Hf : Monotone f) {a : α} {s : Set α} (Ha : IsLeast s a) :
                        IsLeast (f '' s) (f a)

                        A monotone map sends a least element of a set to a least element of its image.

                        theorem Monotone.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (Hf : Monotone f) {a : α} {s : Set α} (Ha : IsGreatest s a) :
                        IsGreatest (f '' s) (f a)

                        A monotone map sends a greatest element of a set to a greatest element of its image.

                        theorem Antitone.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (hf : Antitone f) {a : α} {s : Set α} :
                        a lowerBounds sf a upperBounds (f '' s)
                        theorem Antitone.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (hf : Antitone f) {a : α} {s : Set α} :
                        a upperBounds sf a lowerBounds (f '' s)
                        theorem Antitone.image_lowerBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (hf : Antitone f) {s : Set α} :
                        theorem Antitone.image_upperBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (hf : Antitone f) {s : Set α} :
                        theorem Antitone.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (hf : Antitone f) {s : Set α} :
                        BddAbove sBddBelow (f '' s)

                        The image under an antitone function of a set which is bounded above is bounded below.

                        theorem Antitone.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (hf : Antitone f) {s : Set α} :
                        BddBelow sBddAbove (f '' s)

                        The image under an antitone function of a set which is bounded below is bounded above.

                        theorem Antitone.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (hf : Antitone f) {a : α} {s : Set α} :
                        IsGreatest s aIsLeast (f '' s) (f a)

                        An antitone map sends a greatest element of a set to a least element of its image.

                        theorem Antitone.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (hf : Antitone f) {a : α} {s : Set α} :
                        IsLeast s aIsGreatest (f '' s) (f a)

                        An antitone map sends a least element of a set to a greatest element of its image.

                        theorem mem_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a upperBounds s) (hb : b upperBounds t) :
                        f a b upperBounds (Set.image2 f s t)
                        theorem mem_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a lowerBounds s) (hb : b lowerBounds t) :
                        f a b lowerBounds (Set.image2 f s t)
                        theorem image2_upperBounds_upperBounds_subset {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
                        theorem image2_lowerBounds_lowerBounds_subset {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
                        theorem BddAbove.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
                        BddAbove sBddAbove tBddAbove (Set.image2 f s t)

                        See also Monotone.map_bddAbove.

                        theorem BddBelow.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
                        BddBelow sBddBelow tBddBelow (Set.image2 f s t)

                        See also Monotone.map_bddBelow.

                        theorem IsGreatest.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsGreatest s a) (hb : IsGreatest t b) :
                        IsGreatest (Set.image2 f s t) (f a b)
                        theorem IsLeast.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsLeast s a) (hb : IsLeast t b) :
                        IsLeast (Set.image2 f s t) (f a b)
                        theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a upperBounds s) (hb : b lowerBounds t) :
                        f a b upperBounds (Set.image2 f s t)
                        theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a lowerBounds s) (hb : b upperBounds t) :
                        f a b lowerBounds (Set.image2 f s t)
                        theorem image2_upperBounds_lowerBounds_subset_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
                        theorem image2_lowerBounds_upperBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
                        theorem BddAbove.bddAbove_image2_of_bddBelow {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
                        BddAbove sBddBelow tBddAbove (Set.image2 f s t)
                        theorem BddBelow.bddBelow_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
                        BddBelow sBddAbove tBddBelow (Set.image2 f s t)
                        theorem IsGreatest.isGreatest_image2_of_isLeast {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsGreatest s a) (hb : IsLeast t b) :
                        IsGreatest (Set.image2 f s t) (f a b)
                        theorem IsLeast.isLeast_image2_of_isGreatest {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsLeast s a) (hb : IsGreatest t b) :
                        IsLeast (Set.image2 f s t) (f a b)
                        theorem mem_upperBounds_image2_of_mem_lowerBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a lowerBounds s) (hb : b lowerBounds t) :
                        f a b upperBounds (Set.image2 f s t)
                        theorem mem_lowerBounds_image2_of_mem_upperBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a upperBounds s) (hb : b upperBounds t) :
                        f a b lowerBounds (Set.image2 f s t)
                        theorem image2_upperBounds_upperBounds_subset_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
                        theorem image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
                        theorem BddBelow.image2_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
                        BddBelow sBddBelow tBddAbove (Set.image2 f s t)
                        theorem BddAbove.image2_bddBelow {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) :
                        BddAbove sBddAbove tBddBelow (Set.image2 f s t)
                        theorem IsLeast.isGreatest_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsLeast s a) (hb : IsLeast t b) :
                        IsGreatest (Set.image2 f s t) (f a b)
                        theorem IsGreatest.isLeast_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsGreatest s a) (hb : IsGreatest t b) :
                        IsLeast (Set.image2 f s t) (f a b)
                        theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a lowerBounds s) (hb : b upperBounds t) :
                        f a b upperBounds (Set.image2 f s t)
                        theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a upperBounds s) (hb : b lowerBounds t) :
                        f a b lowerBounds (Set.image2 f s t)
                        theorem image2_lowerBounds_upperBounds_subset_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
                        theorem image2_upperBounds_lowerBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
                        theorem BddBelow.bddAbove_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
                        BddBelow sBddAbove tBddAbove (Set.image2 f s t)
                        theorem BddAbove.bddBelow_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) :
                        BddAbove sBddBelow tBddBelow (Set.image2 f s t)
                        theorem IsLeast.isGreatest_image2_of_isGreatest {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsLeast s a) (hb : IsGreatest t b) :
                        IsGreatest (Set.image2 f s t) (f a b)
                        theorem IsGreatest.isLeast_image2_of_isLeast {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsGreatest s a) (hb : IsLeast t b) :
                        IsLeast (Set.image2 f s t) (f a b)
                        theorem bddAbove_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} :
                        BddAbove s BddAbove (Prod.fst '' s) BddAbove (Prod.snd '' s)
                        theorem bddBelow_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} :
                        BddBelow s BddBelow (Prod.fst '' s) BddBelow (Prod.snd '' s)
                        theorem bddAbove_range_prod {ι : Sort x} {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {F : ια × β} :
                        BddAbove (Set.range F) BddAbove (Set.range (Prod.fst F)) BddAbove (Set.range (Prod.snd F))
                        theorem bddBelow_range_prod {ι : Sort x} {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {F : ια × β} :
                        BddBelow (Set.range F) BddBelow (Set.range (Prod.fst F)) BddBelow (Set.range (Prod.snd F))
                        theorem isLUB_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) :
                        IsLUB s p IsLUB (Prod.fst '' s) p.1 IsLUB (Prod.snd '' s) p.2
                        theorem isGLB_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) :
                        IsGLB s p IsGLB (Prod.fst '' s) p.1 IsGLB (Prod.snd '' s) p.2
                        theorem bddAbove_pi {α : Type u} {π : αType u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} :
                        BddAbove s ∀ (a : α), BddAbove (Function.eval a '' s)
                        theorem bddBelow_pi {α : Type u} {π : αType u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} :
                        BddBelow s ∀ (a : α), BddBelow (Function.eval a '' s)
                        theorem bddAbove_range_pi {α : Type u} {ι : Sort x} {π : αType u_1} [(a : α) → Preorder (π a)] {F : ι(a : α) → π a} :
                        BddAbove (Set.range F) ∀ (a : α), BddAbove (Set.range fun (i : ι) => F i a)
                        theorem bddBelow_range_pi {α : Type u} {ι : Sort x} {π : αType u_1} [(a : α) → Preorder (π a)] {F : ι(a : α) → π a} :
                        BddBelow (Set.range F) ∀ (a : α), BddBelow (Set.range fun (i : ι) => F i a)
                        theorem isLUB_pi {α : Type u} {π : αType u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} {f : (a : α) → π a} :
                        IsLUB s f ∀ (a : α), IsLUB (Function.eval a '' s) (f a)
                        theorem isGLB_pi {α : Type u} {π : αType u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} {f : (a : α) → π a} :
                        IsGLB s f ∀ (a : α), IsGLB (Function.eval a '' s) (f a)
                        theorem IsGLB.of_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (hf : ∀ {x y : α}, f x f y x y) {s : Set α} {x : α} (hx : IsGLB (f '' s) (f x)) :
                        IsGLB s x
                        theorem IsLUB.of_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (hf : ∀ {x y : α}, f x f y x y) {s : Set α} {x : α} (hx : IsLUB (f '' s) (f x)) :
                        IsLUB s x
                        theorem BddAbove.range_mono {α : Type u} {β : Type v} [Preorder β] {f : αβ} (g : αβ) (h : ∀ (a : α), f a g a) (hbdd : BddAbove (Set.range g)) :
                        theorem BddBelow.range_mono {α : Type u} {β : Type v} [Preorder β] (f : αβ) {g : αβ} (h : ∀ (a : α), f a g a) (hbdd : BddBelow (Set.range f)) :
                        theorem BddAbove.range_comp {α : Type u} {β : Type v} {γ : Type u_1} [Preorder β] [Preorder γ] {f : αβ} {g : βγ} (hf : BddAbove (Set.range f)) (hg : Monotone g) :
                        BddAbove (Set.range fun (x : α) => g (f x))
                        theorem BddBelow.range_comp {α : Type u} {β : Type v} {γ : Type u_1} [Preorder β] [Preorder γ] {f : αβ} {g : βγ} (hf : BddBelow (Set.range f)) (hg : Monotone g) :
                        BddBelow (Set.range fun (x : α) => g (f x))
                        def ScottContinuous {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : αβ) :

                        A function between preorders is said to be Scott continuous if it preserves IsLUB on directed sets. It can be shown that a function is Scott continuous if and only if it is continuous wrt the Scott topology.

                        The dual notion

                        ∀ ⦃d : Set α⦄, d.NonemptyDirectedOn (· ≥ ·) d → ∀ ⦃a⦄, IsGLB d a → IsGLB (f '' d) (f a)
                        

                        does not appear to play a significant role in the literature, so is omitted here.

                        Equations
                        Instances For
                          theorem ScottContinuous.monotone {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : αβ} (h : ScottContinuous f) :