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.
Equations
Equations
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
- le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
- sup_le : ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
- inf : α → α → α
- inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
- inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
- le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
- Sup : set α → α
- Inf : set α → α
- le_cSup : ∀ (s : set α) (a : α), bdd_above s → a ∈ s → a ≤ conditionally_complete_lattice.Sup s
- cSup_le : ∀ (s : set α) (a : α), s.nonempty → a ∈ upper_bounds s → conditionally_complete_lattice.Sup s ≤ a
- cInf_le : ∀ (s : set α) (a : α), bdd_below s → a ∈ s → conditionally_complete_lattice.Inf s ≤ a
- le_cInf : ∀ (s : set α) (a : α), s.nonempty → a ∈ lower_bounds s → a ≤ conditionally_complete_lattice.Inf s
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
- conditionally_complete_linear_order.to_conditionally_complete_lattice
- conditionally_complete_linear_order_bot.to_conditionally_complete_lattice
- conditionally_complete_lattice_of_complete_lattice
- order_dual.conditionally_complete_lattice
- with_top.conditionally_complete_lattice
- with_bot.conditionally_complete_lattice
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
- le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
- sup_le : ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
- inf : α → α → α
- inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
- inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
- le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
- Sup : set α → α
- Inf : set α → α
- le_cSup : ∀ (s : set α) (a : α), bdd_above s → a ∈ s → a ≤ conditionally_complete_linear_order.Sup s
- cSup_le : ∀ (s : set α) (a : α), s.nonempty → a ∈ upper_bounds s → conditionally_complete_linear_order.Sup s ≤ a
- cInf_le : ∀ (s : set α) (a : α), bdd_below s → a ∈ s → conditionally_complete_linear_order.Inf s ≤ a
- le_cInf : ∀ (s : set α) (a : α), s.nonempty → a ∈ lower_bounds s → a ≤ conditionally_complete_linear_order.Inf s
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
- le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
- sup_le : ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
- inf : α → α → α
- inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
- inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
- le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
- Sup : set α → α
- Inf : set α → α
- le_cSup : ∀ (s : set α) (a : α), bdd_above s → a ∈ s → a ≤ conditionally_complete_linear_order_bot.Sup s
- cSup_le : ∀ (s : set α) (a : α), s.nonempty → a ∈ upper_bounds s → conditionally_complete_linear_order_bot.Sup s ≤ a
- cInf_le : ∀ (s : set α) (a : α), bdd_below s → a ∈ s → conditionally_complete_linear_order_bot.Inf s ≤ a
- le_cInf : ∀ (s : set α) (a : α), s.nonempty → a ∈ lower_bounds s → a ≤ conditionally_complete_linear_order_bot.Inf s
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
- bot : α
- bot_le : ∀ (a : α), ⊥ ≤ a
- cSup_empty : conditionally_complete_linear_order_bot.Sup ∅ = ⊥
Equations
- conditionally_complete_lattice_of_complete_lattice = {sup := complete_lattice.sup _inst_1, le := complete_lattice.le _inst_1, lt := complete_lattice.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf _inst_1, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup _inst_1, Inf := complete_lattice.Inf _inst_1, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}
Equations
- conditionally_complete_linear_order_of_complete_linear_order = {sup := conditionally_complete_lattice.sup conditionally_complete_lattice_of_complete_lattice, le := conditionally_complete_lattice.le conditionally_complete_lattice_of_complete_lattice, lt := conditionally_complete_lattice.lt conditionally_complete_lattice_of_complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := conditionally_complete_lattice.inf conditionally_complete_lattice_of_complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := conditionally_complete_lattice.Sup conditionally_complete_lattice_of_complete_lattice, Inf := conditionally_complete_lattice.Inf conditionally_complete_lattice_of_complete_lattice, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _, le_total := _, decidable_le := complete_linear_order.decidable_le _inst_1, decidable_eq := complete_linear_order.decidable_eq _inst_1, decidable_lt := complete_linear_order.decidable_lt _inst_1}
A greatest element of a set is the supremum of this set.
A least element of a set is the infimum of this set.
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.
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.
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.
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.
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.
The supremum of a singleton is the element of the singleton
The infimum of a singleton is the element of the singleton
If a set is bounded below and above, and nonempty, its infimum is less than or equal to its supremum.
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.
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.
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.
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.
The supremum of insert a s is the maximum of a and the supremum of s, if s is nonempty and bounded above.
The infimum of insert a s is the minimum of a and the infimum of s, if s is nonempty and bounded below.
The indexed supremum of two functions are comparable if the functions are pointwise comparable
The indexed infimum of two functions are comparable if the functions are pointwise comparable
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.
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.
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.
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.
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'.
This instance is necessary, otherwise the lattice operations would be derived via conditionally_complete_linear_order_bot and marked as noncomputable.
Equations
Equations
- nat.conditionally_complete_linear_order_bot = {sup := lattice.sup lattice_of_decidable_linear_order, le := order_bot.le infer_instance, lt := order_bot.lt infer_instance, le_refl := nat.conditionally_complete_linear_order_bot._proof_1, le_trans := nat.conditionally_complete_linear_order_bot._proof_2, lt_iff_le_not_le := nat.conditionally_complete_linear_order_bot._proof_3, le_antisymm := nat.conditionally_complete_linear_order_bot._proof_4, le_sup_left := nat.conditionally_complete_linear_order_bot._proof_5, le_sup_right := nat.conditionally_complete_linear_order_bot._proof_6, sup_le := nat.conditionally_complete_linear_order_bot._proof_7, inf := lattice.inf lattice_of_decidable_linear_order, inf_le_left := nat.conditionally_complete_linear_order_bot._proof_8, inf_le_right := nat.conditionally_complete_linear_order_bot._proof_9, le_inf := nat.conditionally_complete_linear_order_bot._proof_10, Sup := has_Sup.Sup nat.has_Sup, Inf := has_Inf.Inf nat.has_Inf, le_cSup := nat.conditionally_complete_linear_order_bot._proof_11, cSup_le := nat.conditionally_complete_linear_order_bot._proof_12, cInf_le := nat.conditionally_complete_linear_order_bot._proof_13, le_cInf := nat.conditionally_complete_linear_order_bot._proof_14, le_total := nat.conditionally_complete_linear_order_bot._proof_15, decidable_le := decidable_linear_order.decidable_le infer_instance, decidable_eq := decidable_linear_order.decidable_eq infer_instance, decidable_lt := decidable_linear_order.decidable_lt infer_instance, bot := order_bot.bot infer_instance, bot_le := nat.conditionally_complete_linear_order_bot._proof_16, cSup_empty := nat.conditionally_complete_linear_order_bot._proof_17}
The Sup of a non-empty set is its least upper bound for a conditionally complete lattice with a top.
The Inf of a bounded-below set is its greatest lower bound for a conditionally complete lattice with a top.
Equations
- with_top.complete_linear_order = {sup := lattice.sup with_top.lattice, le := linear_order.le with_top.linear_order, lt := linear_order.lt with_top.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf with_top.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top with_top.order_top, le_top := _, bot := order_bot.bot with_top.order_bot, bot_le := _, Sup := has_Sup.Sup with_top.has_Sup, Inf := has_Inf.Inf with_top.has_Inf, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _, le_total := _, decidable_le := classical.dec_rel has_le.le, decidable_eq := decidable_linear_order.decidable_eq._default linear_order.le linear_order.lt with_top.complete_linear_order._proof_23 with_top.complete_linear_order._proof_24 with_top.complete_linear_order._proof_25 with_top.complete_linear_order._proof_26 with_top.complete_linear_order._proof_27 (classical.dec_rel has_le.le), decidable_lt := decidable_linear_order.decidable_lt._default linear_order.le linear_order.lt with_top.complete_linear_order._proof_28 with_top.complete_linear_order._proof_29 with_top.complete_linear_order._proof_30 with_top.complete_linear_order._proof_31 with_top.complete_linear_order._proof_32 (classical.dec_rel has_le.le)}
Equations
- enat.complete_linear_order = {sup := bounded_lattice.sup enat.bounded_lattice, le := decidable_linear_order.le enat.decidable_linear_order, lt := decidable_linear_order.lt enat.decidable_linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf enat.bounded_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := bounded_lattice.top enat.bounded_lattice, le_top := _, bot := bounded_lattice.bot enat.bounded_lattice, bot_le := _, Sup := λ (s : set enat), ⇑(enat.with_top_equiv.symm) (has_Sup.Sup (⇑enat.with_top_equiv '' s)), Inf := λ (s : set enat), ⇑(enat.with_top_equiv.symm) (has_Inf.Inf (⇑enat.with_top_equiv '' s)), le_Sup := enat.complete_linear_order._proof_1, Sup_le := enat.complete_linear_order._proof_2, Inf_le := enat.complete_linear_order._proof_3, le_Inf := enat.complete_linear_order._proof_4, le_total := _, decidable_le := decidable_linear_order.decidable_le enat.decidable_linear_order, decidable_eq := decidable_linear_order.decidable_eq enat.decidable_linear_order, decidable_lt := decidable_linear_order.decidable_lt enat.decidable_linear_order}
Equations
- order_dual.conditionally_complete_lattice α = {sup := lattice.sup (order_dual.lattice α), le := lattice.le (order_dual.lattice α), lt := lattice.lt (order_dual.lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (order_dual.lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup (order_dual.has_Sup α), Inf := has_Inf.Inf (order_dual.has_Inf α), le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}
Equations
- order_dual.conditionally_complete_linear_order α = {sup := conditionally_complete_lattice.sup (order_dual.conditionally_complete_lattice α), le := conditionally_complete_lattice.le (order_dual.conditionally_complete_lattice α), lt := conditionally_complete_lattice.lt (order_dual.conditionally_complete_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := conditionally_complete_lattice.inf (order_dual.conditionally_complete_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := conditionally_complete_lattice.Sup (order_dual.conditionally_complete_lattice α), Inf := conditionally_complete_lattice.Inf (order_dual.conditionally_complete_lattice α), le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _, le_total := _, decidable_le := decidable_linear_order.decidable_le (order_dual.decidable_linear_order α), decidable_eq := decidable_linear_order.decidable_eq (order_dual.decidable_linear_order α), decidable_lt := decidable_linear_order.decidable_lt (order_dual.decidable_linear_order α)}
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.
Adding a top element to a conditionally complete lattice gives a conditionally complete lattice
Equations
- with_top.conditionally_complete_lattice = {sup := lattice.sup with_top.lattice, le := lattice.le with_top.lattice, lt := lattice.lt with_top.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf with_top.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup with_top.has_Sup, Inf := has_Inf.Inf with_top.has_Inf, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}
Adding a bottom element to a conditionally complete lattice gives a conditionally complete lattice
Equations
- with_bot.conditionally_complete_lattice = {sup := lattice.sup with_bot.lattice, le := lattice.le with_bot.lattice, lt := lattice.lt with_bot.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf with_bot.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup with_bot.has_Sup, Inf := has_Inf.Inf with_bot.has_Inf, le_cSup := _, cSup_le := _, cInf_le := _, le_cInf := _}
Adding a bottom and a top to a conditionally complete lattice gives a bounded lattice
Equations
- with_top.with_bot.bounded_lattice = {sup := lattice.sup (conditionally_complete_lattice.to_lattice (with_top (with_bot α))), le := order_bot.le with_top.order_bot, lt := order_bot.lt with_top.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (conditionally_complete_lattice.to_lattice (with_top (with_bot α))), inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top with_top.order_top, le_top := _, bot := order_bot.bot with_top.order_bot, bot_le := _}
Equations
- with_top.with_bot.complete_lattice = {sup := bounded_lattice.sup with_top.with_bot.bounded_lattice, le := bounded_lattice.le with_top.with_bot.bounded_lattice, lt := bounded_lattice.lt with_top.with_bot.bounded_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf with_top.with_bot.bounded_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := bounded_lattice.top with_top.with_bot.bounded_lattice, le_top := _, bot := bounded_lattice.bot with_top.with_bot.bounded_lattice, bot_le := _, Sup := has_Sup.Sup with_top.has_Sup, Inf := has_Inf.Inf with_top.has_Inf, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}