mathlib documentation

order.conditionally_complete_lattice

Theory of conditionally complete lattices.

A conditionally complete lattice is a lattice in which every non-empty bounded subset s has a least upper bound and a greatest lower bound, denoted below by Sup s and Inf s. Typical examples are real, nat, int with their usual orders.

The theory is very comparable to the theory of complete lattices, except that suitable boundedness and nonemptiness assumptions have to be added to most statements. We introduce two predicates bdd_above and bdd_below to express this boundedness, prove their basic properties, and then go on to prove most useful properties of Sup and Inf in conditionally complete lattices.

To differentiate the statements between complete lattices and conditionally complete lattices, we prefix Inf and Sup in the statements by c, giving cInf and cSup. For instance, Inf_le is a statement in complete lattices ensuring Inf s ≤ x, while cInf_le is the same statement in conditionally complete lattices with an additional assumption that s is bounded below.

Extension of Sup and Inf from a preorder α to with_top α and with_bot α

@[instance]
def with_top.has_Sup {α : Type u_1} [preorder α] [has_Sup α] :

Equations
@[instance]
def with_top.has_Inf {α : Type u_1} [has_Inf α] :

Equations
@[instance]
def with_bot.has_Sup {α : Type u_1} [has_Sup α] :

Equations
@[instance]
def with_bot.has_Inf {α : Type u_1} [preorder α] [has_Inf α] :

Equations
@[class]
structure conditionally_complete_lattice  :
Type u_4Type u_4

A conditionally complete lattice is a lattice in which every nonempty subset which is bounded above has a supremum, and every nonempty subset which is bounded below has an infimum. Typical examples are real numbers or natural numbers.

To differentiate the statements from the corresponding statements in (unconditional) complete lattices, we prefix Inf and Sup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.

Instances
@[class]
structure conditionally_complete_linear_order  :
Type u_4Type u_4

A conditionally complete linear order is a linear order in which every nonempty subset which is bounded above has a supremum, and every nonempty subset which is bounded below has an infimum. Typical examples are real numbers or natural numbers.

To differentiate the statements from the corresponding statements in (unconditional) complete linear orders, we prefix Inf and Sup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.

Instances
@[class]
structure conditionally_complete_linear_order_bot  :
Type u_4Type u_4

A conditionally complete linear order with bot is a linear order with least element, in which every nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily bounded below) has an infimum. A typical example is the natural numbers.

To differentiate the statements from the corresponding statements in (unconditional) complete linear orders, we prefix Inf and Sup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.

Instances
theorem le_cSup {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
bdd_above sa sa Sup s

theorem cSup_le {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
s.nonempty(∀ (b : α), b sb a)Sup s a

theorem cInf_le {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
bdd_below sa sInf s a

theorem le_cInf {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
s.nonempty(∀ (b : α), b sa b)a Inf s

theorem le_cSup_of_le {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a b : α} :
bdd_above sb sa ba Sup s

theorem cInf_le_of_le {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a b : α} :
bdd_below sb sb aInf s a

theorem cSup_le_cSup {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} :
bdd_above ts.nonemptys tSup s Sup t

theorem cInf_le_cInf {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} :
bdd_below ts.nonemptys tInf t Inf s

theorem is_lub_cSup {α : Type u_1} [conditionally_complete_lattice α] {s : set α} :
s.nonemptybdd_above sis_lub s (Sup s)

theorem is_glb_cInf {α : Type u_1} [conditionally_complete_lattice α] {s : set α} :
s.nonemptybdd_below sis_glb s (Inf s)

theorem is_lub.cSup_eq {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
is_lub s as.nonemptySup s = a

theorem is_greatest.cSup_eq {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
is_greatest s aSup s = a

A greatest element of a set is the supremum of this set.

theorem is_glb.cInf_eq {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
is_glb s as.nonemptyInf s = a

theorem is_least.cInf_eq {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
is_least s aInf s = a

A least element of a set is the infimum of this set.

theorem subset_Icc_cInf_cSup {α : Type u_1} [conditionally_complete_lattice α] {s : set α} :
bdd_below sbdd_above ss set.Icc (Inf s) (Sup s)

theorem cSup_le_iff {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
bdd_above ss.nonempty(Sup s a ∀ (b : α), b sb a)

theorem le_cInf_iff {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
bdd_below ss.nonempty(a Inf s ∀ (b : α), b sa b)

theorem cSup_lower_bounds_eq_cInf {α : Type u_1} [conditionally_complete_lattice α] {s : set α} :

theorem cInf_upper_bounds_eq_cSup {α : Type u_1} [conditionally_complete_lattice α] {s : set α} :

theorem cSup_intro {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {b : α} :
s.nonempty(∀ (a : α), a sa b)(∀ (w : α), w < b(∃ (a : α) (H : a s), w < a))Sup s = b

Introduction rule to prove that b is the supremum of s: it suffices to check that b is larger than all elements of s, and that this is not the case of any w<b.

theorem cInf_intro {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {b : α} :
s.nonempty(∀ (a : α), a sb a)(∀ (w : α), b < w(∃ (a : α) (H : a s), a < w))Inf s = b

Introduction rule to prove that b is the infimum of s: it suffices to check that b is smaller than all elements of s, and that this is not the case of any w>b.

theorem lt_cSup_of_lt {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a b : α} :
bdd_above sa sb < ab < Sup s

b < Sup s when there is an element a in s with b < a, when s is bounded above. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness above for one direction, nonemptiness and linear order for the other one), so we formulate separately the two implications, contrary to the complete_lattice case.

theorem cInf_lt_of_lt {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a b : α} :
bdd_below sa sa < bInf s < b

Inf s < b when there is an element a in s with a < b, when s is bounded below. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness below for one direction, nonemptiness and linear order for the other one), so we formulate separately the two implications, contrary to the complete_lattice case.

theorem exists_between_of_forall_le {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} :
s.nonemptyt.nonempty(∀ (x : α), x s∀ (y : α), y tx y)(upper_bounds s lower_bounds t).nonempty

If all elements of a nonempty set s are less than or equal to all elements of a nonempty set t, then there exists an element between these sets.

@[simp]
theorem cSup_singleton {α : Type u_1} [conditionally_complete_lattice α] (a : α) :
Sup {a} = a

The supremum of a singleton is the element of the singleton

@[simp]
theorem cInf_singleton {α : Type u_1} [conditionally_complete_lattice α] (a : α) :
Inf {a} = a

The infimum of a singleton is the element of the singleton

theorem cInf_le_cSup {α : Type u_1} [conditionally_complete_lattice α] {s : set α} :
bdd_below sbdd_above ss.nonemptyInf s Sup s

If a set is bounded below and above, and nonempty, its infimum is less than or equal to its supremum.

theorem cSup_union {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} :
bdd_above ss.nonemptybdd_above tt.nonemptySup (s t) = Sup s Sup t

The sup of a union of two sets is the max of the suprema of each subset, under the assumptions that all sets are bounded above and nonempty.

theorem cInf_union {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} :
bdd_below ss.nonemptybdd_below tt.nonemptyInf (s t) = Inf s Inf t

The inf of a union of two sets is the min of the infima of each subset, under the assumptions that all sets are bounded below and nonempty.

theorem cSup_inter_le {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} :
bdd_above sbdd_above t(s t).nonemptySup (s t) Sup s Sup t

The supremum of an intersection of two sets is bounded by the minimum of the suprema of each set, if all sets are bounded above and nonempty.

theorem le_cInf_inter {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} :
bdd_below sbdd_below t(s t).nonemptyInf s Inf t Inf (s t)

The infimum of an intersection of two sets is bounded below by the maximum of the infima of each set, if all sets are bounded below and nonempty.

theorem cSup_insert {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
bdd_above ss.nonemptySup (insert a s) = a Sup s

The supremum of insert a s is the maximum of a and the supremum of s, if s is nonempty and bounded above.

theorem cInf_insert {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} :
bdd_below ss.nonemptyInf (insert a s) = a Inf s

The infimum of insert a s is the minimum of a and the infimum of s, if s is nonempty and bounded below.

@[simp]
theorem cInf_Ici {α : Type u_1} [conditionally_complete_lattice α] {a : α} :
Inf (set.Ici a) = a

@[simp]
theorem cSup_Iic {α : Type u_1} [conditionally_complete_lattice α] {a : α} :
Sup (set.Iic a) = a

theorem csupr_le_csupr {α : Type u_1} {ι : Sort u_3} [conditionally_complete_lattice α] {f g : ι → α} :
bdd_above (set.range g)(∀ (x : ι), f x g x)supr f supr g

The indexed supremum of two functions are comparable if the functions are pointwise comparable

theorem csupr_le {α : Type u_1} {ι : Sort u_3} [conditionally_complete_lattice α] [nonempty ι] {f : ι → α} {c : α} :
(∀ (x : ι), f x c)supr f c

The indexed supremum of a function is bounded above by a uniform bound

theorem le_csupr {α : Type u_1} {ι : Sort u_3} [conditionally_complete_lattice α] {f : ι → α} (H : bdd_above (set.range f)) (c : ι) :
f c supr f

The indexed supremum of a function is bounded below by the value taken at one point

theorem cinfi_le_cinfi {α : Type u_1} {ι : Sort u_3} [conditionally_complete_lattice α] {f g : ι → α} :
bdd_below (set.range f)(∀ (x : ι), f x g x)infi f infi g

The indexed infimum of two functions are comparable if the functions are pointwise comparable

theorem le_cinfi {α : Type u_1} {ι : Sort u_3} [conditionally_complete_lattice α] [nonempty ι] {f : ι → α} {c : α} :
(∀ (x : ι), c f x)c infi f

The indexed minimum of a function is bounded below by a uniform lower bound

theorem cinfi_le {α : Type u_1} {ι : Sort u_3} [conditionally_complete_lattice α] {f : ι → α} (H : bdd_below (set.range f)) (c : ι) :
infi f f c

The indexed infimum of a function is bounded above by the value taken at one point

@[simp]
theorem cinfi_const {α : Type u_1} {ι : Sort u_3} [conditionally_complete_lattice α] [hι : nonempty ι] {a : α} :
(⨅ (b : ι), a) = a

@[simp]
theorem csupr_const {α : Type u_1} {ι : Sort u_3} [conditionally_complete_lattice α] [hι : nonempty ι] {a : α} :
(⨆ (b : ι), a) = a

theorem exists_lt_of_lt_cSup {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} {b : α} :
s.nonemptyb < Sup s(∃ (a : α) (H : a s), b < a)

When b < Sup s, there is an element a in s with b < a, if s is nonempty and the order is a linear order.

theorem exists_lt_of_lt_csupr {α : Type u_1} {ι : Sort u_3} [conditionally_complete_linear_order α] {b : α} [nonempty ι] {f : ι → α} :
b < supr f(∃ (i : ι), b < f i)

Indexed version of the above lemma exists_lt_of_lt_cSup. When b < supr f, there is an element i such that b < f i.

theorem exists_lt_of_cInf_lt {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} {b : α} :
s.nonemptyInf s < b(∃ (a : α) (H : a s), a < b)

When Inf s < b, there is an element a in s with a < b, if s is nonempty and the order is a linear order.

theorem exists_lt_of_cinfi_lt {α : Type u_1} {ι : Sort u_3} [conditionally_complete_linear_order α] {a : α} [nonempty ι] {f : ι → α} :
infi f < a(∃ (i : ι), f i < a)

Indexed version of the above lemma exists_lt_of_cInf_lt When infi f < a, there is an element i such that f i < a.

theorem cSup_intro' {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} {b : α} :
s.nonempty(∀ (a : α), a sa b)(∀ (ub : α), (∀ (a : α), a sa ub)b ub)Sup s = b

Introduction rule to prove that b is the supremum of s: it suffices to check that 1) b is an upper bound 2) every other upper bound b' satisfies b ≤ b'.

@[instance]

Equations
@[instance]

Equations
theorem nat.Inf_def {s : set } (h : s.nonempty) :

theorem nat.Sup_def {s : set } (h : ∃ (n : ), ∀ (a : ), a sa n) :

@[simp]
theorem nat.Inf_eq_zero {s : set } :
Inf s = 0 0 s s =

theorem nat.Inf_mem {s : set } :
s.nonemptyInf s s

theorem nat.not_mem_of_lt_Inf {s : set } {m : } :
m < Inf sm s

theorem nat.Inf_le {s : set } {m : } :
m sInf s m

@[instance]

This instance is necessary, otherwise the lattice operations would be derived via conditionally_complete_linear_order_bot and marked as noncomputable.

Equations
@[instance]

Equations
theorem with_top.is_lub_Sup' {β : Type u_1} [conditionally_complete_lattice β] {s : set (with_top β)} :
s.nonemptyis_lub s (Sup s)

The Sup of a non-empty set is its least upper bound for a conditionally complete lattice with a top.

theorem with_top.is_lub_Sup {α : Type u_1} [conditionally_complete_linear_order_bot α] (s : set (with_top α)) :
is_lub s (Sup s)

theorem with_top.is_glb_Inf' {β : Type u_1} [conditionally_complete_lattice β] {s : set (with_top β)} :
bdd_below sis_glb s (Inf s)

The Inf of a bounded-below set is its greatest lower bound for a conditionally complete lattice with a top.

theorem with_top.is_glb_Inf {α : Type u_1} [conditionally_complete_linear_order_bot α] (s : set (with_top α)) :
is_glb s (Inf s)

@[instance]

Equations
theorem with_top.coe_Sup {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} :
bdd_above s((Sup s) = ⨆ (a : α) (H : a s), a)

theorem with_top.coe_Inf {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} :
s.nonempty((Inf s) = ⨅ (a : α) (H : a s), a)

A monotone function into a conditionally complete lattice preserves the ordering properties of Sup and Inf.

theorem monotone.le_cSup_image {α : Type u_1} {β : Type u_2} [preorder α] [conditionally_complete_lattice β] {f : α → β} (h_mono : monotone f) {s : set α} {c : α} :
c sbdd_above sf c Sup (f '' s)

theorem monotone.cSup_image_le {α : Type u_1} {β : Type u_2} [preorder α] [conditionally_complete_lattice β] {f : α → β} (h_mono : monotone f) {s : set α} (hs : s.nonempty) {B : α} :
B upper_bounds sSup (f '' s) f B

theorem monotone.cInf_image_le {α : Type u_1} {β : Type u_2} [preorder α] [conditionally_complete_lattice β] {f : α → β} (h_mono : monotone f) {s : set α} {c : α} :
c sbdd_below sInf (f '' s) f c

theorem monotone.le_cInf_image {α : Type u_1} {β : Type u_2} [preorder α] [conditionally_complete_lattice β] {f : α → β} (h_mono : monotone f) {s : set α} (hs : s.nonempty) {B : α} :
B lower_bounds sf B Inf (f '' s)

Complete lattice structure on with_top (with_bot α)

If α is a conditionally_complete_lattice, then we show that with_top α and with_bot α also inherit the structure of conditionally complete lattices. Furthermore, we show that with_top (with_bot α) naturally inherits the structure of a complete lattice. Note that for α a conditionally complete lattice, Sup and Inf both return junk values for sets which are empty or unbounded. The extension of Sup to with_top α fixes the unboundedness problem and the extension to with_bot α fixes the problem with the empty set.

This result can be used to show that the extended reals [-∞, ∞] are a complete lattice.

@[instance]

Adding a top element to a conditionally complete lattice gives a conditionally complete lattice

Equations
@[instance]

Adding a bottom element to a conditionally complete lattice gives a conditionally complete lattice

Equations

### Subtypes of conditionally complete linear orders

In this section we give conditions on a subset of a conditionally complete linear order, to ensure that the subtype is itself conditionally complete.

We check that an ord_connected set satisfies these conditions.

TODO There are several possible variants; the conditionally_complete_linear_order could be changed to conditionally_complete_linear_order_bot or complete_linear_order.

def subset_has_Sup {α : Type u_1} (s : set α) [has_Sup α] [inhabited s] :

has_Sup structure on a nonempty subset s of an object with has_Sup. This definition is non-canonical (it uses default s); it should be used only as here, as an auxiliary instance in the construction of the conditionally_complete_linear_order structure.

Equations
@[simp]
theorem subset_Sup_def {α : Type u_1} (s : set α) [has_Sup α] [inhabited s] :
Sup = λ (t : set s), dite (Sup (coe '' t) s) (λ (ht : Sup (coe '' t) s), Sup (coe '' t), ht⟩) (λ (ht : Sup (coe '' t) s), default s)

theorem subset_Sup_of_within {α : Type u_1} (s : set α) [has_Sup α] [inhabited s] {t : set s} :
Sup (coe '' t) sSup (coe '' t) = (Sup t)

def subset_has_Inf {α : Type u_1} (s : set α) [has_Inf α] [inhabited s] :

has_Inf structure on a nonempty subset s of an object with has_Inf. This definition is non-canonical (it uses default s); it should be used only as here, as an auxiliary instance in the construction of the conditionally_complete_linear_order structure.

Equations
@[simp]
theorem subset_Inf_def {α : Type u_1} (s : set α) [has_Inf α] [inhabited s] :
Inf = λ (t : set s), dite (Inf (coe '' t) s) (λ (ht : Inf (coe '' t) s), Inf (coe '' t), ht⟩) (λ (ht : Inf (coe '' t) s), default s)

theorem subset_Inf_of_within {α : Type u_1} (s : set α) [has_Inf α] [inhabited s] {t : set s} :
Inf (coe '' t) sInf (coe '' t) = (Inf t)

def subset_conditionally_complete_linear_order {α : Type u_1} (s : set α) [conditionally_complete_linear_order α] [inhabited s] :
(∀ {t : set s}, t.nonemptybdd_above tSup (coe '' t) s)(∀ {t : set s}, t.nonemptybdd_below tInf (coe '' t) s)conditionally_complete_linear_order s

For a nonempty subset of a conditionally complete linear order to be a conditionally complete linear order, it suffices that it contain the Sup of all its nonempty bounded-above subsets, and the Inf of all its nonempty bounded-below subsets.

Equations
theorem Sup_within_of_ord_connected {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} [hs : s.ord_connected] ⦃t : set s⦄ :
t.nonemptybdd_above tSup (coe '' t) s

The Sup function on a nonempty ord_connected set s in a conditionally complete linear order takes values within s, for all nonempty bounded-above subsets of s.

theorem Inf_within_of_ord_connected {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} [hs : s.ord_connected] ⦃t : set s⦄ :
t.nonemptybdd_below tInf (coe '' t) s

The Inf function on a nonempty ord_connected set s in a conditionally complete linear order takes values within s, for all nonempty bounded-below subsets of s.