order.bounds

Upper / lower bounds #

In this file we define:

• `upper_bounds`, `lower_bounds` : the set of upper bounds (resp., lower bounds) of a set;
• `bdd_above s`, `bdd_below s` : the set `s` is bounded above (resp., below), i.e., the set of upper (resp., lower) bounds of `s` is nonempty;
• `is_least s a`, `is_greatest s a` : `a` is a least (resp., greatest) element of `s`; for a partial order, it is unique if exists;
• `is_lub s a`, `is_glb s a` : `a` is a least upper bound (resp., a greatest lower bound) of `s`; for a partial order, it is unique if exists.

We also prove various lemmas about monotonicity, behaviour under `∪`, `∩`, `insert`, and provide formulas for `∅`, `univ`, and intervals.

Definitions #

def upper_bounds {α : Type u} [preorder α] (s : set α) :
set α

The set of upper bounds of a set.

Equations
• = {x : α | ∀ ⦃a : α⦄, a sa x}
def lower_bounds {α : Type u} [preorder α] (s : set α) :
set α

The set of lower bounds of a set.

Equations
• = {x : α | ∀ ⦃a : α⦄, a sx a}
def bdd_above {α : Type u} [preorder α] (s : set α) :
Prop

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

Equations
def bdd_below {α : Type u} [preorder α] (s : set α) :
Prop

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

Equations
def is_least {α : Type u} [preorder α] (s : set α) (a : α) :
Prop

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

Equations
def is_greatest {α : Type u} [preorder α] (s : set α) (a : α) :
Prop

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

Equations
def is_lub {α : 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
def is_glb {α : 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
theorem mem_upper_bounds {α : Type u} [preorder α] {s : set α} {a : α} :
∀ (x : α), x sx a
theorem mem_lower_bounds {α : Type u} [preorder α] {s : set α} {a : α} :
∀ (x : α), x sa x
theorem bdd_above_def {α : Type u} [preorder α] {s : set α} :
∃ (x : α), ∀ (y : α), y sy x
theorem bdd_below_def {α : Type u} [preorder α] {s : set α} :
∃ (x : α), ∀ (y : α), y sx y
theorem bot_mem_lower_bounds {α : Type u} [preorder α] [order_bot α] (s : set α) :
theorem top_mem_upper_bounds {α : Type u} [preorder α] [order_top α] (s : set α) :
@[simp]
theorem is_least_bot_iff {α : Type u} [preorder α] {s : set α} [order_bot α] :
@[simp]
theorem is_greatest_top_iff {α : Type u} [preorder α] {s : set α} [order_top α] :
theorem not_bdd_above_iff' {α : Type u} [preorder α] {s : set α} :
∀ (x : α), ∃ (y : α) (H : y s), ¬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_bdd_above_iff`.

theorem not_bdd_below_iff' {α : Type u} [preorder α] {s : set α} :
∀ (x : α), ∃ (y : α) (H : y s), ¬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_bdd_below_iff`.

theorem not_bdd_above_iff {α : Type u_1} [linear_order α] {s : set α} :
∀ (x : α), ∃ (y : α) (H : y s), 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_bdd_above_iff'`.

theorem not_bdd_below_iff {α : Type u_1} [linear_order α] {s : set α} :
∀ (x : α), ∃ (y : α) (H : y s), 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_bdd_below_iff'`.

theorem bdd_above.dual {α : Type u} [preorder α] {s : set α} (h : bdd_above s) :
theorem bdd_below.dual {α : Type u} [preorder α] {s : set α} (h : bdd_below s) :
theorem is_least.dual {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
theorem is_greatest.dual {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
theorem is_lub.dual {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
theorem is_glb.dual {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
@[reducible]
def is_least.order_bot {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :

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

Equations
@[reducible]
def is_greatest.order_top {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :

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

Equations

Monotonicity #

theorem upper_bounds_mono_set {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s t) :
theorem lower_bounds_mono_set {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s t) :
theorem upper_bounds_mono_mem {α : Type u} [preorder α] {s : set α} ⦃a b : α⦄ (hab : a b) :
theorem lower_bounds_mono_mem {α : Type u} [preorder α] {s : set α} ⦃a b : α⦄ (hab : a b) :
theorem upper_bounds_mono {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s t) ⦃a b : α⦄ (hab : a b) :
theorem lower_bounds_mono {α : Type u} [preorder α] ⦃s t : set α⦄ (hst : s t) ⦃a b : α⦄ (hab : a b) :
theorem bdd_above.mono {α : Type u} [preorder α] ⦃s t : set α⦄ (h : s t) :

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

theorem bdd_below.mono {α : Type u} [preorder α] ⦃s t : set α⦄ (h : s t) :

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

theorem is_lub.of_subset_of_superset {α : Type u} [preorder α] {a : α} {s t p : set α} (hs : a) (hp : a) (hst : s t) (htp : t p) :
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 is_glb.of_subset_of_superset {α : Type u} [preorder α] {a : α} {s t p : set α} (hs : a) (hp : a) (hst : s t) (htp : t p) :
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 is_least.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : a) (hb : b) (hst : s t) :
b a
theorem is_greatest.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : a) (hb : b) (hst : s t) :
a b
theorem is_lub.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : a) (hb : b) (hst : s t) :
a b
theorem is_glb.mono {α : Type u} [preorder α] {s t : set α} {a b : α} (ha : a) (hb : b) (hst : s t) :
b a
theorem subset_lower_bounds_upper_bounds {α : Type u} [preorder α] (s : set α) :
theorem subset_upper_bounds_lower_bounds {α : Type u} [preorder α] (s : set α) :
theorem set.nonempty.bdd_above_lower_bounds {α : Type u} [preorder α] {s : set α} (hs : s.nonempty) :
theorem set.nonempty.bdd_below_upper_bounds {α : Type u} [preorder α] {s : set α} (hs : s.nonempty) :

Conversions #

theorem is_least.is_glb {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
a
theorem is_greatest.is_lub {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
a
theorem is_lub.upper_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
theorem is_glb.lower_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
theorem is_least.lower_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
theorem is_greatest.upper_bounds_eq {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
theorem is_lub_le_iff {α : Type u} [preorder α] {s : set α} {a b : α} (h : a) :
a b
theorem le_is_glb_iff {α : Type u} [preorder α] {s : set α} {a b : α} (h : a) :
b a
theorem is_lub_iff_le_iff {α : Type u} [preorder α] {s : set α} {a : α} :
a ∀ (b : α), a b
theorem is_glb_iff_le_iff {α : Type u} [preorder α] {s : set α} {a : α} :
a ∀ (b : α), b a
theorem is_lub.bdd_above {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :

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

theorem is_glb.bdd_below {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :

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

theorem is_greatest.bdd_above {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :

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

theorem is_least.bdd_below {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :

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

theorem is_least.nonempty {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :
theorem is_greatest.nonempty {α : Type u} [preorder α] {s : set α} {a : α} (h : a) :

Union and intersection #

@[simp]
theorem upper_bounds_union {α : Type u} [preorder α] {s t : set α} :
@[simp]
theorem lower_bounds_union {α : Type u} [preorder α] {s t : set α} :
theorem union_upper_bounds_subset_upper_bounds_inter {α : Type u} [preorder α] {s t : set α} :
theorem union_lower_bounds_subset_lower_bounds_inter {α : Type u} [preorder α] {s t : set α} :
theorem is_least_union_iff {α : Type u} [preorder α] {a : α} {s t : set α} :
is_least (s t) a a a
theorem is_greatest_union_iff {α : Type u} [preorder α] {s t : set α} {a : α} :
theorem bdd_above.inter_of_left {α : Type u} [preorder α] {s t : set α} (h : bdd_above s) :

If `s` is bounded, then so is `s ∩ t`

theorem bdd_above.inter_of_right {α : Type u} [preorder α] {s t : set α} (h : bdd_above t) :

If `t` is bounded, then so is `s ∩ t`

theorem bdd_below.inter_of_left {α : Type u} [preorder α] {s t : set α} (h : bdd_below s) :

If `s` is bounded, then so is `s ∩ t`

theorem bdd_below.inter_of_right {α : Type u} [preorder α] {s t : set α} (h : bdd_below t) :

If `t` is bounded, then so is `s ∩ t`

theorem bdd_above.union {γ : Type w} {s t : set γ} :
bdd_above (s t)

If `s` and `t` are bounded above sets in a `semilattice_sup`, then so is `s ∪ t`.

theorem bdd_above_union {γ : Type w} {s t : set γ} :

The union of two sets is bounded above if and only if each of the sets is.

theorem bdd_below.union {γ : Type w} {s t : set γ} :
bdd_below (s t)
theorem bdd_below_union {γ : Type w} {s t : set γ} :

The union of two sets is bounded above if and only if each of the sets is.

theorem is_lub.union {γ : Type w} {a b : γ} {s t : set γ} (hs : a) (ht : b) :
is_lub (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 is_glb.union {γ : Type w} {a₁ a₂ : γ} {s t : set γ} (hs : a₁) (ht : a₂) :
is_glb (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 is_least.union {γ : Type w} [linear_order γ] {a b : γ} {s t : set γ} (ha : a) (hb : b) :
is_least (s t) 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 is_greatest.union {γ : Type w} [linear_order γ] {a b : γ} {s t : set γ} (ha : a) (hb : b) :
is_greatest (s t) 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 is_lub.inter_Ici_of_mem {γ : Type w} [linear_order γ] {s : set γ} {a b : γ} (ha : a) (hb : b s) :
theorem is_glb.inter_Iic_of_mem {γ : Type w} [linear_order γ] {s : set γ} {a b : γ} (ha : a) (hb : b s) :
theorem bdd_above_iff_exists_ge {γ : Type w} {s : set γ} (x₀ : γ) :
∃ (x : γ), x₀ x ∀ (y : γ), y sy x
theorem bdd_below_iff_exists_le {γ : Type w} {s : set γ} (x₀ : γ) :
∃ (x : γ), x x₀ ∀ (y : γ), y sx y
theorem bdd_above.exists_ge {γ : Type w} {s : set γ} (hs : bdd_above s) (x₀ : γ) :
∃ (x : γ), x₀ x ∀ (y : γ), y sy x
theorem bdd_below.exists_le {γ : Type w} {s : set γ} (hs : bdd_below s) (x₀ : γ) :
∃ (x : γ), x x₀ ∀ (y : γ), y sx y

Specific sets #

Unbounded intervals #

theorem is_least_Ici {α : Type u} [preorder α] {a : α} :
theorem is_greatest_Iic {α : Type u} [preorder α] {a : α} :
a
theorem is_lub_Iic {α : Type u} [preorder α] {a : α} :
theorem is_glb_Ici {α : Type u} [preorder α] {a : α} :
theorem upper_bounds_Iic {α : Type u} [preorder α] {a : α} :
=
theorem lower_bounds_Ici {α : Type u} [preorder α] {a : α} :
=
theorem bdd_above_Iic {α : Type u} [preorder α] {a : α} :
theorem bdd_below_Ici {α : Type u} [preorder α] {a : α} :
theorem bdd_above_Iio {α : Type u} [preorder α] {a : α} :
theorem bdd_below_Ioi {α : Type u} [preorder α] {a : α} :
theorem lub_Iio_le {α : Type u} [preorder α] {b : α} (a : α) (hb : is_lub (set.Iio a) b) :
b a
theorem le_glb_Ioi {α : Type u} [preorder α] {b : α} (a : α) (hb : is_glb (set.Ioi a) b) :
a b
theorem lub_Iio_eq_self_or_Iio_eq_Iic {γ : Type w} {j : γ} (i : γ) (hj : is_lub (set.Iio i) j) :
j = i =
theorem glb_Ioi_eq_self_or_Ioi_eq_Ici {γ : Type w} {j : γ} (i : γ) (hj : is_glb (set.Ioi i) j) :
j = i =
theorem exists_lub_Iio {γ : Type w} [linear_order γ] (i : γ) :
∃ (j : γ), is_lub (set.Iio i) j
theorem exists_glb_Ioi {γ : Type w} [linear_order γ] (i : γ) :
∃ (j : γ), is_glb (set.Ioi i) j
theorem is_lub_Iio {γ : Type w} [linear_order γ] {a : γ} :
theorem is_glb_Ioi {γ : Type w} [linear_order γ] {a : γ} :
theorem upper_bounds_Iio {γ : Type w} [linear_order γ] {a : γ} :
=
theorem lower_bounds_Ioi {γ : Type w} [linear_order γ] {a : γ} :
=

Singleton #

theorem is_greatest_singleton {α : Type u} [preorder α] {a : α} :
theorem is_least_singleton {α : Type u} [preorder α] {a : α} :
is_least {a} a
theorem is_lub_singleton {α : Type u} [preorder α] {a : α} :
is_lub {a} a
theorem is_glb_singleton {α : Type u} [preorder α] {a : α} :
is_glb {a} a
theorem bdd_above_singleton {α : Type u} [preorder α] {a : α} :
theorem bdd_below_singleton {α : Type u} [preorder α] {a : α} :
@[simp]
theorem upper_bounds_singleton {α : Type u} [preorder α] {a : α} :
@[simp]
theorem lower_bounds_singleton {α : Type u} [preorder α] {a : α} :

Bounded intervals #

theorem bdd_above_Icc {α : Type u} [preorder α] {a b : α} :
theorem bdd_below_Icc {α : Type u} [preorder α] {a b : α} :
theorem bdd_above_Ico {α : Type u} [preorder α] {a b : α} :
theorem bdd_below_Ico {α : Type u} [preorder α] {a b : α} :
theorem bdd_above_Ioc {α : Type u} [preorder α] {a b : α} :
theorem bdd_below_Ioc {α : Type u} [preorder α] {a b : α} :
theorem bdd_above_Ioo {α : Type u} [preorder α] {a b : α} :
theorem bdd_below_Ioo {α : Type u} [preorder α] {a b : α} :
theorem is_greatest_Icc {α : Type u} [preorder α] {a b : α} (h : a b) :
theorem is_lub_Icc {α : Type u} [preorder α] {a b : α} (h : a b) :
is_lub (set.Icc a b) b
theorem upper_bounds_Icc {α : Type u} [preorder α] {a b : α} (h : a b) :
theorem is_least_Icc {α : Type u} [preorder α] {a b : α} (h : a b) :
theorem is_glb_Icc {α : Type u} [preorder α] {a b : α} (h : a b) :
is_glb (set.Icc a b) a
theorem lower_bounds_Icc {α : Type u} [preorder α] {a b : α} (h : a b) :
theorem is_greatest_Ioc {α : Type u} [preorder α] {a b : α} (h : a < b) :
theorem is_lub_Ioc {α : Type u} [preorder α] {a b : α} (h : a < b) :
is_lub (set.Ioc a b) b
theorem upper_bounds_Ioc {α : Type u} [preorder α] {a b : α} (h : a < b) :
theorem is_least_Ico {α : Type u} [preorder α] {a b : α} (h : a < b) :
theorem is_glb_Ico {α : Type u} [preorder α] {a b : α} (h : a < b) :
is_glb (set.Ico a b) a
theorem lower_bounds_Ico {α : Type u} [preorder α] {a b : α} (h : a < b) :
theorem is_glb_Ioo {γ : Type w} {a b : γ} (h : a < b) :
is_glb (set.Ioo a b) a
theorem lower_bounds_Ioo {γ : Type w} {a b : γ} (hab : a < b) :
theorem is_glb_Ioc {γ : Type w} {a b : γ} (hab : a < b) :
is_glb (set.Ioc a b) a
theorem lower_bound_Ioc {γ : Type w} {a b : γ} (hab : a < b) :
theorem is_lub_Ioo {γ : Type w} {a b : γ} (hab : a < b) :
is_lub (set.Ioo a b) b
theorem upper_bounds_Ioo {γ : Type w} {a b : γ} (hab : a < b) :
theorem is_lub_Ico {γ : Type w} {a b : γ} (hab : a < b) :
is_lub (set.Ico a b) b
theorem upper_bounds_Ico {γ : Type w} {a b : γ} (hab : a < b) :
theorem bdd_below_iff_subset_Ici {α : Type u} [preorder α] {s : set α} :
∃ (a : α), s
theorem bdd_above_iff_subset_Iic {α : Type u} [preorder α] {s : set α} :
∃ (a : α), s
theorem bdd_below_bdd_above_iff_subset_Icc {α : Type u} [preorder α] {s : set α} :
∃ (a b : α), s b

Univ #

theorem is_greatest_univ {γ : Type w} [preorder γ] [order_top γ] :
@[simp]
theorem order_top.upper_bounds_univ {γ : Type w} [order_top γ] :
theorem is_lub_univ {γ : Type w} [preorder γ] [order_top γ] :
@[simp]
theorem order_bot.lower_bounds_univ {γ : Type w} [order_bot γ] :
theorem is_least_univ {γ : Type w} [preorder γ] [order_bot γ] :
theorem is_glb_univ {γ : Type w} [preorder γ] [order_bot γ] :
@[simp]
theorem no_max_order.upper_bounds_univ {α : Type u} [preorder α] [no_max_order α] :
@[simp]
theorem no_min_order.lower_bounds_univ {α : Type u} [preorder α] [no_min_order α] :
@[simp]
theorem not_bdd_above_univ {α : Type u} [preorder α] [no_max_order α] :
@[simp]
theorem not_bdd_below_univ {α : Type u} [preorder α] [no_min_order α] :

Empty set #

@[simp]
theorem upper_bounds_empty {α : Type u} [preorder α] :
@[simp]
theorem lower_bounds_empty {α : Type u} [preorder α] :
@[simp]
theorem bdd_above_empty {α : Type u} [preorder α] [nonempty α] :
@[simp]
theorem bdd_below_empty {α : Type u} [preorder α] [nonempty α] :
theorem is_glb_empty {γ : Type w} [preorder γ] [order_top γ] :
theorem is_lub_empty {γ : Type w} [preorder γ] [order_bot γ] :
theorem is_lub.nonempty {α : Type u} [preorder α] {s : set α} {a : α} [no_min_order α] (hs : a) :
theorem is_glb.nonempty {α : Type u} [preorder α] {s : set α} {a : α} [no_max_order α] (hs : a) :
theorem nonempty_of_not_bdd_above {α : Type u} [preorder α] {s : set α} [ha : nonempty α] (h : ¬) :
theorem nonempty_of_not_bdd_below {α : Type u} [preorder α] {s : set α} [ha : nonempty α] (h : ¬) :

insert #

@[simp]
theorem bdd_above_insert {γ : Type w} (a : γ) {s : set γ} :

Adding a point to a set preserves its boundedness above.

theorem bdd_above.insert {γ : Type w} (a : γ) {s : set γ} (hs : bdd_above s) :
@[simp]
theorem bdd_below_insert {γ : Type w} (a : γ) {s : set γ} :

Adding a point to a set preserves its boundedness below.

theorem bdd_below.insert {γ : Type w} (a : γ) {s : set γ} (hs : bdd_below s) :
theorem is_lub.insert {γ : Type w} (a : γ) {b : γ} {s : set γ} (hs : b) :
is_lub s) (a b)
theorem is_glb.insert {γ : Type w} (a : γ) {b : γ} {s : set γ} (hs : b) :
is_glb s) (a b)
theorem is_greatest.insert {γ : Type w} [linear_order γ] (a : γ) {b : γ} {s : set γ} (hs : b) :
b)
theorem is_least.insert {γ : Type w} [linear_order γ] (a : γ) {b : γ} {s : set γ} (hs : b) :
b)
@[simp]
theorem upper_bounds_insert {α : Type u} [preorder α] (a : α) (s : set α) :
=
@[simp]
theorem lower_bounds_insert {α : Type u} [preorder α] (a : α) (s : set α) :
=
@[protected, simp]
theorem order_top.bdd_above {γ : Type w} [preorder γ] [order_top γ] (s : set γ) :

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

@[protected, simp]
theorem order_bot.bdd_below {γ : Type w} [preorder γ] [order_bot γ] (s : set γ) :

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

Pair #

theorem is_lub_pair {γ : Type w} {a b : γ} :
is_lub {a, b} (a b)
theorem is_glb_pair {γ : Type w} {a b : γ} :
is_glb {a, b} (a b)
theorem is_least_pair {γ : Type w} [linear_order γ] {a b : γ} :
is_least {a, b} b)
theorem is_greatest_pair {γ : Type w} [linear_order γ] {a b : γ} :
is_greatest {a, b} b)

Lower/upper bounds #

@[simp]
theorem is_lub_lower_bounds {α : Type u} [preorder α] {s : set α} {a : α} :
a a
@[simp]
theorem is_glb_upper_bounds {α : Type u} [preorder α] {s : set α} {a : α} :
a a

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

theorem lower_bounds_le_upper_bounds {α : Type u} [preorder α] {s : set α} {a b : α} (ha : a ) (hb : b ) :
s.nonemptya b
theorem is_glb_le_is_lub {α : Type u} [preorder α] {s : set α} {a b : α} (ha : a) (hb : b) (hs : s.nonempty) :
a b
theorem is_lub_lt_iff {α : Type u} [preorder α] {s : set α} {a b : α} (ha : a) :
a < b ∃ (c : α) (H : c , c < b
theorem lt_is_glb_iff {α : Type u} [preorder α] {s : set α} {a b : α} (ha : a) :
b < a ∃ (c : α) (H : c , b < c
theorem le_of_is_lub_le_is_glb {α : Type u} [preorder α] {s : set α} {a b x y : α} (ha : a) (hb : b) (hab : b a) (hx : x s) (hy : y s) :
x y
theorem is_least.unique {α : Type u} {s : set α} {a b : α} (Ha : a) (Hb : b) :
a = b
theorem is_least.is_least_iff_eq {α : Type u} {s : set α} {a b : α} (Ha : a) :
b a = b
theorem is_greatest.unique {α : Type u} {s : set α} {a b : α} (Ha : a) (Hb : b) :
a = b
theorem is_greatest.is_greatest_iff_eq {α : Type u} {s : set α} {a b : α} (Ha : a) :
b a = b
theorem is_lub.unique {α : Type u} {s : set α} {a b : α} (Ha : a) (Hb : b) :
a = b
theorem is_glb.unique {α : Type u} {s : set α} {a b : α} (Ha : a) (Hb : b) :
a = b
theorem set.subsingleton_of_is_lub_le_is_glb {α : Type u} {s : set α} {a b : α} (Ha : a) (Hb : b) (hab : b a) :
theorem is_glb_lt_is_lub_of_ne {α : Type u} {s : set α} {a b : α} (Ha : a) (Hb : b) {x y : α} (Hx : x s) (Hy : y s) (Hxy : x y) :
a < b
theorem lt_is_lub_iff {α : Type u} [linear_order α] {s : set α} {a b : α} (h : a) :
b < a ∃ (c : α) (H : c s), b < c
theorem is_glb_lt_iff {α : Type u} [linear_order α] {s : set α} {a b : α} (h : a) :
a < b ∃ (c : α) (H : c s), c < b
theorem is_lub.exists_between {α : Type u} [linear_order α] {s : set α} {a b : α} (h : a) (hb : b < a) :
∃ (c : α) (H : c s), b < c c a
theorem is_lub.exists_between' {α : Type u} [linear_order α] {s : set α} {a b : α} (h : a) (h' : a s) (hb : b < a) :
∃ (c : α) (H : c s), b < c c < a
theorem is_glb.exists_between {α : Type u} [linear_order α] {s : set α} {a b : α} (h : a) (hb : a < b) :
∃ (c : α) (H : c s), a c c < b
theorem is_glb.exists_between' {α : Type u} [linear_order α] {s : set α} {a b : α} (h : a) (h' : a s) (hb : a < b) :
∃ (c : α) (H : c s), a < c c < b

Least upper bound and the greatest lower bound in linear ordered additive commutative groups #

theorem is_glb.exists_between_self_add {α : Type u} {s : set α} {a ε : α} (h : a) (hε : 0 < ε) :
∃ (b : α) (H : b s), a b b < a + ε
theorem is_glb.exists_between_self_add' {α : Type u} {s : set α} {a ε : α} (h : a) (h₂ : a s) (hε : 0 < ε) :
∃ (b : α) (H : b s), a < b b < a + ε
theorem is_lub.exists_between_sub_self {α : Type u} {s : set α} {a ε : α} (h : a) (hε : 0 < ε) :
∃ (b : α) (H : b s), a - ε < b b a
theorem is_lub.exists_between_sub_self' {α : Type u} {s : set α} {a ε : α} (h : a) (h₂ : a s) (hε : 0 < ε) :
∃ (b : α) (H : b s), a - ε < b b < a

Images of upper/lower bounds under monotone functions #

theorem monotone_on.mem_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) {a : α} (Hst : s t) (Has : a ) (Hat : a t) :
f a upper_bounds (f '' s)
theorem monotone_on.mem_upper_bounds_image_self {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : t) {a : α} :
a tf a upper_bounds (f '' t)
theorem monotone_on.mem_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) {a : α} (Hst : s t) (Has : a ) (Hat : a t) :
f a lower_bounds (f '' s)
theorem monotone_on.mem_lower_bounds_image_self {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : t) {a : α} :
a tf a lower_bounds (f '' t)
theorem monotone_on.image_upper_bounds_subset_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) (Hst : s t) :
f '' t) upper_bounds (f '' s)
theorem monotone_on.image_lower_bounds_subset_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) (Hst : s t) :
f '' t) lower_bounds (f '' s)
theorem monotone_on.map_bdd_above {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) (Hst : s t) :
t).nonemptybdd_above (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 monotone_on.map_bdd_below {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) (Hst : s t) :
t).nonemptybdd_below (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 monotone_on.map_is_least {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : t) {a : α} (Ha : a) :
is_least (f '' t) (f a)

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

theorem monotone_on.map_is_greatest {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : t) {a : α} (Ha : a) :
is_greatest (f '' t) (f a)

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

theorem antitone_on.mem_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) {a : α} (Hst : s t) (Has : a ) :
a tf a upper_bounds (f '' s)
theorem antitone_on.mem_upper_bounds_image_self {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : t) {a : α} :
a tf a upper_bounds (f '' t)
theorem antitone_on.mem_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) {a : α} (Hst : s t) :
a tf a lower_bounds (f '' s)
theorem antitone_on.mem_lower_bounds_image_self {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : t) {a : α} :
a tf a lower_bounds (f '' t)
theorem antitone_on.image_lower_bounds_subset_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) (Hst : s t) :
f '' t) upper_bounds (f '' s)
theorem antitone_on.image_upper_bounds_subset_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) (Hst : s t) :
f '' t) lower_bounds (f '' s)
theorem antitone_on.map_bdd_above {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) (Hst : s t) :
t).nonemptybdd_below (f '' s)

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

theorem antitone_on.map_bdd_below {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {s t : set α} (Hf : t) (Hst : s t) :
t).nonemptybdd_above (f '' s)

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

theorem antitone_on.map_is_greatest {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : t) {a : α} :
ais_least (f '' t) (f a)

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

theorem antitone_on.map_is_least {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} {t : set α} (Hf : t) {a : α} :
ais_greatest (f '' t) (f a)

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

theorem monotone.mem_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} (Ha : a ) :
f a upper_bounds (f '' s)
theorem monotone.mem_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} (Ha : a ) :
f a lower_bounds (f '' s)
theorem monotone.image_upper_bounds_subset_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {s : set α} :
theorem monotone.image_lower_bounds_subset_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {s : set α} :
theorem monotone.map_bdd_above {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {s : set α} :
bdd_above (f '' s)

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

theorem monotone.map_bdd_below {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {s : set α} :
bdd_below (f '' s)

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

theorem monotone.map_is_least {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} (Ha : a) :
is_least (f '' s) (f a)

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

theorem monotone.map_is_greatest {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) {a : α} {s : set α} (Ha : a) :
is_greatest (f '' s) (f a)

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

theorem antitone.mem_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {a : α} {s : set α} :
f a upper_bounds (f '' s)
theorem antitone.mem_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {a : α} {s : set α} :
f a lower_bounds (f '' s)
theorem antitone.image_lower_bounds_subset_upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {s : set α} :
theorem antitone.image_upper_bounds_subset_lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {s : set α} :
theorem antitone.map_bdd_above {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {s : set α} :
bdd_below (f '' s)

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

theorem antitone.map_bdd_below {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {s : set α} :
bdd_above (f '' s)

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

theorem antitone.map_is_greatest {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {a : α} {s : set α} :
ais_least (f '' s) (f a)

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

theorem antitone.map_is_least {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : antitone f) {a : α} {s : set α} :
ais_greatest (f '' s) (f a)

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

theorem mem_upper_bounds_image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), monotone (f a)) (ha : a ) (hb : b ) :
f a b upper_bounds s t)
theorem mem_lower_bounds_image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), monotone (f a)) (ha : a ) (hb : b ) :
f a b lower_bounds s t)
theorem image2_upper_bounds_upper_bounds_subset {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), monotone (f a)) :
theorem image2_lower_bounds_lower_bounds_subset {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), monotone (f a)) :
theorem bdd_above.image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), monotone (f a)) :
bdd_above s t)

See also `monotone.map_bdd_above`.

theorem bdd_below.image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), monotone (f a)) :
bdd_below s t)

See also `monotone.map_bdd_below`.

theorem is_greatest.image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), monotone (f a)) (ha : a) (hb : b) :
is_greatest s t) (f a b)
theorem is_least.image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), monotone (f a)) (ha : a) (hb : b) :
is_least s t) (f a b)
theorem mem_upper_bounds_image2_of_mem_upper_bounds_of_mem_lower_bounds {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), antitone (f a)) (ha : a ) (hb : b ) :
f a b upper_bounds s t)
theorem mem_lower_bounds_image2_of_mem_lower_bounds_of_mem_upper_bounds {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), antitone (f a)) (ha : a ) (hb : b ) :
f a b lower_bounds s t)
theorem image2_upper_bounds_lower_bounds_subset_upper_bounds_image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), antitone (f a)) :
theorem image2_lower_bounds_upper_bounds_subset_lower_bounds_image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), antitone (f a)) :
theorem bdd_above.bdd_above_image2_of_bdd_below {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), antitone (f a)) :
bdd_above s t)
theorem bdd_below.bdd_below_image2_of_bdd_above {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), antitone (f a)) :
bdd_below s t)
theorem is_greatest.is_greatest_image2_of_is_least {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), antitone (f a)) (ha : a) (hb : b) :
is_greatest s t) (f a b)
theorem is_least.is_least_image2_of_is_greatest {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), monotone b)) (h₁ : ∀ (a : α), antitone (f a)) (ha : a) (hb : b) :
is_least s t) (f a b)
theorem mem_upper_bounds_image2_of_mem_lower_bounds {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), antitone (f a)) (ha : a ) (hb : b ) :
f a b upper_bounds s t)
theorem mem_lower_bounds_image2_of_mem_upper_bounds {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), antitone (f a)) (ha : a ) (hb : b ) :
f a b lower_bounds s t)
theorem image2_upper_bounds_upper_bounds_subset_upper_bounds_image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), antitone (f a)) :
theorem image2_lower_bounds_lower_bounds_subset_lower_bounds_image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), antitone (f a)) :
theorem bdd_below.image2_bdd_above {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), antitone (f a)) :
bdd_above s t)
theorem bdd_above.image2_bdd_below {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), antitone (f a)) :
bdd_below s t)
theorem is_least.is_greatest_image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), antitone (f a)) (ha : a) (hb : b) :
is_greatest s t) (f a b)
theorem is_greatest.is_least_image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), antitone (f a)) (ha : a) (hb : b) :
is_least s t) (f a b)
theorem mem_upper_bounds_image2_of_mem_upper_bounds_of_mem_upper_bounds {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), monotone (f a)) (ha : a ) (hb : b ) :
f a b upper_bounds s t)
theorem mem_lower_bounds_image2_of_mem_lower_bounds_of_mem_lower_bounds {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), monotone (f a)) (ha : a ) (hb : b ) :
f a b lower_bounds s t)
theorem image2_lower_bounds_upper_bounds_subset_upper_bounds_image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), monotone (f a)) :
theorem image2_upper_bounds_lower_bounds_subset_lower_bounds_image2 {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), monotone (f a)) :
theorem bdd_below.bdd_above_image2_of_bdd_above {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), monotone (f a)) :
bdd_above s t)
theorem bdd_above.bdd_below_image2_of_bdd_above {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), monotone (f a)) :
bdd_below s t)
theorem is_least.is_greatest_image2_of_is_greatest {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), monotone (f a)) (ha : a) (hb : b) :
is_greatest s t) (f a b)
theorem is_greatest.is_least_image2_of_is_least {α : Type u} {β : Type v} {γ : Type w} [preorder α] [preorder β] [preorder γ] {f : α → β → γ} {s : set α} {t : set β} {a : α} {b : β} (h₀ : ∀ (b : β), antitone b)) (h₁ : ∀ (a : α), monotone (f a)) (ha : a) (hb : b) :
is_least s t) (f a b)
theorem is_glb.of_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : ∀ {x y : α}, f x f y x y) {s : set α} {x : α} (hx : is_glb (f '' s) (f x)) :
x
theorem is_lub.of_image {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : ∀ {x y : α}, f x f y x y) {s : set α} {x : α} (hx : is_lub (f '' s) (f x)) :
x
theorem is_lub_pi {α : Type u} {π : α → Type u_1} [Π (a : α), preorder (π a)] {s : set (Π (a : α), π a)} {f : Π (a : α), π a} :
f ∀ (a : α), is_lub '' s) (f a)
theorem is_glb_pi {α : Type u} {π : α → Type u_1} [Π (a : α), preorder (π a)] {s : set (Π (a : α), π a)} {f : Π (a : α), π a} :
f ∀ (a : α), is_glb '' s) (f a)
theorem is_lub_prod {α : Type u} {β : Type v} [preorder α] [preorder β] {s : set × β)} (p : α × β) :
theorem is_glb_prod {α : Type u} {β : Type v} [preorder α] [preorder β] {s : set × β)} (p : α × β) :
theorem order_iso.upper_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α ≃o β) {s : set α} :
theorem order_iso.lower_bounds_image {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α ≃o β) {s : set α} :
@[simp]
theorem order_iso.is_lub_image {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : β} :
is_lub (f '' s) x ((f.symm) x)
theorem order_iso.is_lub_image' {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : α} :
is_lub (f '' s) (f x) x
@[simp]
theorem order_iso.is_glb_image {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : β} :
is_glb (f '' s) x ((f.symm) x)
theorem order_iso.is_glb_image' {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α ≃o β) {s : set α} {x : α} :
is_glb (f '' s) (f x) x
@[simp]
theorem order_iso.is_lub_preimage {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : α} :
is_lub (f ⁻¹' s) x (f x)
theorem order_iso.is_lub_preimage' {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : β} :
is_lub (f ⁻¹' s) ((f.symm) x) x
@[simp]
theorem order_iso.is_glb_preimage {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : α} :
is_glb (f ⁻¹' s) x (f x)
theorem order_iso.is_glb_preimage' {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α ≃o β) {s : set β} {x : β} :
is_glb (f ⁻¹' s) ((f.symm) x) x