mathlib3 documentation

order.conditionally_complete_lattice.basic

Theory of conditionally complete lattices. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ℝ, ℕ, and ℤ 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 α

source
@[protected, instance]
noncomputable def with_top.has_Sup {α : Type u_1} [preorder α] [has_Sup α] :
has_Sup (with_top α)
Equations
source
@[protected, instance]
noncomputable def with_top.has_Inf {α : Type u_1} [has_Inf α] :
has_Inf (with_top α)
Equations
source
@[protected, instance]
noncomputable def with_bot.has_Sup {α : Type u_1} [has_Sup α] :
has_Sup (with_bot α)
Equations
source
@[protected, instance]
noncomputable def with_bot.has_Inf {α : Type u_1} [preorder α] [has_Inf α] :
has_Inf (with_bot α)
Equations
source
theorem with_top.Sup_eq {α : Type u_1} [preorder α] [has_Sup α] {s : set (with_top α)} (hs : ⊤ ∉ s) (hs' : bdd_above (coe ⁻¹' s)) :
has_Sup.Sup s = ↑(has_Sup.Sup (coe ⁻¹' s))
source
theorem with_top.Inf_eq {α : Type u_1} [has_Inf α] {s : set (with_top α)} (hs : ¬s ⊆ {⊤}) :
has_Inf.Inf s = ↑(has_Inf.Inf (coe ⁻¹' s))
source
theorem with_bot.Inf_eq {α : Type u_1} [preorder α] [has_Inf α] {s : set (with_bot α)} (hs : ⊥ ∉ s) (hs' : bdd_below (coe ⁻¹' s)) :
has_Inf.Inf s = ↑(has_Inf.Inf (coe ⁻¹' s))
source
theorem with_bot.Sup_eq {α : Type u_1} [has_Sup α] {s : set (with_bot α)} (hs : ¬s ⊆ {⊥}) :
has_Sup.Sup s = ↑(has_Sup.Sup (coe ⁻¹' s))
source
@[simp]
theorem with_top.cInf_empty {α : Type u_1} [has_Inf α] :
has_Inf.Inf ∅ = ⊤
source
@[simp]
theorem with_top.cinfi_empty {ι : Sort u_4} {α : Type u_1} [is_empty ι] [has_Inf α] (f : ι → with_top α) :
(⨅ (i : ι), f i) = ⊤
source
theorem with_top.coe_Inf' {α : Type u_1} [has_Inf α] {s : set α} (hs : s.nonempty) :
↑(has_Inf.Inf s) = has_Inf.Inf (coe '' s)
source
@[norm_cast]
theorem with_top.coe_infi {α : Type u_1} {ι : Sort u_4} [nonempty ι] [has_Inf α] (f : ι → α) :
(↑⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)
source
theorem with_top.coe_Sup' {α : Type u_1} [preorder α] [has_Sup α] {s : set α} (hs : bdd_above s) :
↑(has_Sup.Sup s) = has_Sup.Sup (coe '' s)
source
@[norm_cast]
theorem with_top.coe_supr {α : Type u_1} {ι : Sort u_4} [preorder α] [has_Sup α] (f : ι → α) (h : bdd_above (set.range f)) :
(↑⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)
source
@[simp]
theorem with_bot.cSup_empty {α : Type u_1} [has_Sup α] :
has_Sup.Sup ∅ = ⊥
source
@[simp]
theorem with_bot.csupr_empty {ι : Sort u_4} {α : Type u_1} [is_empty ι] [has_Sup α] (f : ι → with_bot α) :
(⨆ (i : ι), f i) = ⊥
source
@[norm_cast]
theorem with_bot.coe_Sup' {α : Type u_1} [has_Sup α] {s : set α} (hs : s.nonempty) :
↑(has_Sup.Sup s) = has_Sup.Sup (coe '' s)
source
@[norm_cast]
theorem with_bot.coe_supr {α : Type u_1} {ι : Sort u_4} [nonempty ι] [has_Sup α] (f : ι → α) :
(↑⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)
source
@[norm_cast]
theorem with_bot.coe_Inf' {α : Type u_1} [preorder α] [has_Inf α] {s : set α} (hs : bdd_below s) :
↑(has_Inf.Inf s) = has_Inf.Inf (coe '' s)
source
@[norm_cast]
theorem with_bot.coe_infi {α : Type u_1} {ι : Sort u_4} [preorder α] [has_Inf α] (f : ι → α) (h : bdd_below (set.range f)) :
(↑⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)
source
@[instance]
def conditionally_complete_lattice.to_has_Inf (α : Type u_5) [self : conditionally_complete_lattice α] :
has_Inf α
source
@[instance]
def conditionally_complete_lattice.to_has_Sup (α : Type u_5) [self : conditionally_complete_lattice α] :
has_Sup α
source
@[instance]
def conditionally_complete_lattice.to_lattice (α : Type u_5) [self : conditionally_complete_lattice α] :
lattice α
source
@[class]
structure conditionally_complete_lattice (α : Type u_5) :
Type u_5

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 of this typeclass
Instances of other typeclasses for conditionally_complete_lattice
  • conditionally_complete_lattice.has_sizeof_inst
source
@[class]
structure conditionally_complete_linear_order (α : Type u_5) :
Type u_5

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 of this typeclass
Instances of other typeclasses for conditionally_complete_linear_order
  • conditionally_complete_linear_order.has_sizeof_inst
source
@[instance]
def conditionally_complete_linear_order.to_conditionally_complete_lattice (α : Type u_5) [self : conditionally_complete_linear_order α] :
conditionally_complete_lattice α
source
@[instance]
def conditionally_complete_linear_order.to_linear_order (α : Type u_5) [self : conditionally_complete_linear_order α] :
linear_order α
source
@[instance]
def conditionally_complete_linear_order_bot.to_has_bot (α : Type u_5) [self : conditionally_complete_linear_order_bot α] :
has_bot α
source
@[instance]
def conditionally_complete_linear_order_bot.to_conditionally_complete_linear_order (α : Type u_5) [self : conditionally_complete_linear_order_bot α] :
conditionally_complete_linear_order α
source
@[class]
structure conditionally_complete_linear_order_bot (α : Type u_5) :
Type u_5

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 of this typeclass
Instances of other typeclasses for conditionally_complete_linear_order_bot
  • conditionally_complete_linear_order_bot.has_sizeof_inst
source
@[protected, instance]
def conditionally_complete_linear_order_bot.to_order_bot {α : Type u_1} [h : conditionally_complete_linear_order_bot α] :
order_bot α
Equations
source
@[protected, instance]
def complete_lattice.to_conditionally_complete_lattice {α : Type u_1} [complete_lattice α] :
conditionally_complete_lattice α

A complete lattice is a conditionally complete lattice, as there are no restrictions on the properties of Inf and Sup in a complete lattice.

Equations
source
@[protected, instance]
def complete_linear_order.to_conditionally_complete_linear_order_bot {α : Type u_1} [complete_linear_order α] :
conditionally_complete_linear_order_bot α
Equations
source
@[reducible]
noncomputable def is_well_order.conditionally_complete_linear_order_bot (α : Type u_1) [i₁ : linear_order α] [i₂ : order_bot α] [h : is_well_order α has_lt.lt] :
conditionally_complete_linear_order_bot α

A well founded linear order is conditionally complete, with a bottom element.

Equations
source
@[protected, instance]
def order_dual.conditionally_complete_lattice (α : Type u_1) [conditionally_complete_lattice α] :
conditionally_complete_lattice αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.conditionally_complete_linear_order (α : Type u_1) [conditionally_complete_linear_order α] :
conditionally_complete_linear_order αᵒᵈ
Equations
source
def conditionally_complete_lattice_of_Sup (α : Type u_1) [H1 : partial_order α] [H2 : has_Sup α] (bdd_above_pair : ∀ (a b : α), bdd_above {a, b}) (bdd_below_pair : ∀ (a b : α), bdd_below {a, b}) (is_lub_Sup : ∀ (s : set α), bdd_above s → s.nonempty → is_lub s (has_Sup.Sup s)) :
conditionally_complete_lattice α

Create a conditionally_complete_lattice from a partial_order and Sup function that returns the least upper bound of a nonempty set which is bounded above. Usually this constructor provides poor definitional equalities. If other fields are known explicitly, they should be provided; for example, if inf is known explicitly, construct the conditionally_complete_lattice instance as

instance : conditionally_complete_lattice my_T :=
{ inf := better_inf,
  le_inf := ...,
  inf_le_right := ...,
  inf_le_left := ...
  -- don't care to fix sup, Inf
  ..conditionally_complete_lattice_of_Sup my_T _ }
Equations
source
def conditionally_complete_lattice_of_Inf (α : Type u_1) [H1 : partial_order α] [H2 : has_Inf α] (bdd_above_pair : ∀ (a b : α), bdd_above {a, b}) (bdd_below_pair : ∀ (a b : α), bdd_below {a, b}) (is_glb_Inf : ∀ (s : set α), bdd_below s → s.nonempty → is_glb s (has_Inf.Inf s)) :
conditionally_complete_lattice α

Create a conditionally_complete_lattice_of_Inf from a partial_order and Inf function that returns the greatest lower bound of a nonempty set which is bounded below. Usually this constructor provides poor definitional equalities. If other fields are known explicitly, they should be provided; for example, if inf is known explicitly, construct the conditionally_complete_lattice instance as

instance : conditionally_complete_lattice my_T :=
{ inf := better_inf,
  le_inf := ...,
  inf_le_right := ...,
  inf_le_left := ...
  -- don't care to fix sup, Sup
  ..conditionally_complete_lattice_of_Inf my_T _ }
Equations
source
def conditionally_complete_lattice_of_lattice_of_Sup (α : Type u_1) [H1 : lattice α] [H2 : has_Sup α] (is_lub_Sup : ∀ (s : set α), bdd_above s → s.nonempty → is_lub s (has_Sup.Sup s)) :
conditionally_complete_lattice α

A version of conditionally_complete_lattice_of_Sup when we already know that α is a lattice.

This should only be used when it is both hard and unnecessary to provide Inf explicitly.

Equations
source
def conditionally_complete_lattice_of_lattice_of_Inf (α : Type u_1) [H1 : lattice α] [H2 : has_Inf α] (is_glb_Inf : ∀ (s : set α), bdd_below s → s.nonempty → is_glb s (has_Inf.Inf s)) :
conditionally_complete_lattice α

A version of conditionally_complete_lattice_of_Inf when we already know that α is a lattice.

This should only be used when it is both hard and unnecessary to provide Sup explicitly.

Equations
source
theorem le_cSup {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (h₁ : bdd_above s) (h₂ : a ∈ s) :
a ≤ has_Sup.Sup s
source
theorem cSup_le {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (h₁ : s.nonempty) (h₂ : ∀ (b : α), b ∈ s → b ≤ a) :
has_Sup.Sup s ≤ a
source
theorem cInf_le {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (h₁ : bdd_below s) (h₂ : a ∈ s) :
has_Inf.Inf s ≤ a
source
theorem le_cInf {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (h₁ : s.nonempty) (h₂ : ∀ (b : α), b ∈ s → a ≤ b) :
a ≤ has_Inf.Inf s
source
theorem le_cSup_of_le {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a b : α} (hs : bdd_above s) (hb : b ∈ s) (h : a ≤ b) :
a ≤ has_Sup.Sup s
source
theorem cInf_le_of_le {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a b : α} (hs : bdd_below s) (hb : b ∈ s) (h : b ≤ a) :
has_Inf.Inf s ≤ a
source
theorem cSup_le_cSup {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} (ht : bdd_above t) (hs : s.nonempty) (h : s ⊆ t) :
has_Sup.Sup s ≤ has_Sup.Sup t
source
theorem cInf_le_cInf {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} (ht : bdd_below t) (hs : s.nonempty) (h : s ⊆ t) :
has_Inf.Inf t ≤ has_Inf.Inf s
source
theorem le_cSup_iff {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (h : bdd_above s) (hs : s.nonempty) :
a ≤ has_Sup.Sup s ↔ ∀ (b : α), b ∈ upper_bounds s → a ≤ b
source
theorem cInf_le_iff {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (h : bdd_below s) (hs : s.nonempty) :
has_Inf.Inf s ≤ a ↔ ∀ (b : α), b ∈ lower_bounds s → b ≤ a
source
theorem is_lub_cSup {α : Type u_1} [conditionally_complete_lattice α] {s : set α} (ne : s.nonempty) (H : bdd_above s) :
is_lub s (has_Sup.Sup s)
source
theorem is_lub_csupr {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] [nonempty ι] {f : ι → α} (H : bdd_above (set.range f)) :
is_lub (set.range f) (⨆ (i : ι), f i)
source
theorem is_lub_csupr_set {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] {f : β → α} {s : set β} (H : bdd_above (f '' s)) (Hne : s.nonempty) :
is_lub (f '' s) (⨆ (i : ↥s), f ↑i)
source
theorem is_glb_cInf {α : Type u_1} [conditionally_complete_lattice α] {s : set α} (ne : s.nonempty) (H : bdd_below s) :
is_glb s (has_Inf.Inf s)
source
theorem is_glb_cinfi {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] [nonempty ι] {f : ι → α} (H : bdd_below (set.range f)) :
is_glb (set.range f) (⨅ (i : ι), f i)
source
theorem is_glb_cinfi_set {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] {f : β → α} {s : set β} (H : bdd_below (f '' s)) (Hne : s.nonempty) :
is_glb (f '' s) (⨅ (i : ↥s), f ↑i)
source
theorem csupr_le_iff {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] [nonempty ι] {f : ι → α} {a : α} (hf : bdd_above (set.range f)) :
supr f ≤ a ↔ ∀ (i : ι), f i ≤ a
source
theorem le_cinfi_iff {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] [nonempty ι] {f : ι → α} {a : α} (hf : bdd_below (set.range f)) :
a ≤ infi f ↔ ∀ (i : ι), a ≤ f i
source
theorem csupr_set_le_iff {α : Type u_1} [conditionally_complete_lattice α] {ι : Type u_2} {s : set ι} {f : ι → α} {a : α} (hs : s.nonempty) (hf : bdd_above (f '' s)) :
(⨆ (i : ↥s), f ↑i) ≤ a ↔ ∀ (i : ι), i ∈ s → f i ≤ a
source
theorem le_cinfi_set_iff {α : Type u_1} [conditionally_complete_lattice α] {ι : Type u_2} {s : set ι} {f : ι → α} {a : α} (hs : s.nonempty) (hf : bdd_below (f '' s)) :
(a ≤ ⨅ (i : ↥s), f ↑i) ↔ ∀ (i : ι), i ∈ s → a ≤ f i
source
theorem is_lub.cSup_eq {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (H : is_lub s a) (ne : s.nonempty) :
has_Sup.Sup s = a
source
theorem is_lub.csupr_eq {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] {a : α} [nonempty ι] {f : ι → α} (H : is_lub (set.range f) a) :
(⨆ (i : ι), f i) = a
source
theorem is_lub.csupr_set_eq {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] {a : α} {s : set β} {f : β → α} (H : is_lub (f '' s) a) (Hne : s.nonempty) :
(⨆ (i : ↥s), f ↑i) = a
source
theorem is_greatest.cSup_eq {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (H : is_greatest s a) :
has_Sup.Sup s = a

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

source
theorem is_greatest.Sup_mem {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (H : is_greatest s a) :
has_Sup.Sup s ∈ s
source
theorem is_glb.cInf_eq {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (H : is_glb s a) (ne : s.nonempty) :
has_Inf.Inf s = a
source
theorem is_glb.cinfi_eq {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] {a : α} [nonempty ι] {f : ι → α} (H : is_glb (set.range f) a) :
(⨅ (i : ι), f i) = a
source
theorem is_glb.cinfi_set_eq {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] {a : α} {s : set β} {f : β → α} (H : is_glb (f '' s) a) (Hne : s.nonempty) :
(⨅ (i : ↥s), f ↑i) = a
source
theorem is_least.cInf_eq {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (H : is_least s a) :
has_Inf.Inf s = a

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

source
theorem is_least.Inf_mem {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (H : is_least s a) :
has_Inf.Inf s ∈ s
source
theorem subset_Icc_cInf_cSup {α : Type u_1} [conditionally_complete_lattice α] {s : set α} (hb : bdd_below s) (ha : bdd_above s) :
s ⊆ set.Icc (has_Inf.Inf s) (has_Sup.Sup s)
source
theorem cSup_le_iff {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (hb : bdd_above s) (hs : s.nonempty) :
has_Sup.Sup s ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a
source
theorem le_cInf_iff {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (hb : bdd_below s) (hs : s.nonempty) :
a ≤ has_Inf.Inf s ↔ ∀ (b : α), b ∈ s → a ≤ b
source
theorem cSup_lower_bounds_eq_cInf {α : Type u_1} [conditionally_complete_lattice α] {s : set α} (h : bdd_below s) (hs : s.nonempty) :
has_Sup.Sup (lower_bounds s) = has_Inf.Inf s
source
theorem cInf_upper_bounds_eq_cSup {α : Type u_1} [conditionally_complete_lattice α] {s : set α} (h : bdd_above s) (hs : s.nonempty) :
has_Inf.Inf (upper_bounds s) = has_Sup.Sup s
source
theorem not_mem_of_lt_cInf {α : Type u_1} [conditionally_complete_lattice α] {x : α} {s : set α} (h : x < has_Inf.Inf s) (hs : bdd_below s) :
x ∉ s
source
theorem not_mem_of_cSup_lt {α : Type u_1} [conditionally_complete_lattice α] {x : α} {s : set α} (h : has_Sup.Sup s < x) (hs : bdd_above s) :
x ∉ s
source
theorem cSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {b : α} (hs : s.nonempty) (H : ∀ (a : α), a ∈ s → a ≤ b) (H' : ∀ (w : α), w < b → (∃ (a : α) (H : a ∈ s), w < a)) :
has_Sup.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. See Sup_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.

source
theorem cInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {b : α} :
s.nonempty → (∀ (a : α), a ∈ s → b ≤ a) → (∀ (w : α), b < w → (∃ (a : α) (H : a ∈ s), a < w)) → has_Inf.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. See Inf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.

source
theorem lt_cSup_of_lt {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a b : α} (hs : bdd_above s) (ha : a ∈ s) (h : b < a) :
b < has_Sup.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.

source
theorem cInf_lt_of_lt {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a b : α} :
bdd_below s → a ∈ s → a < b → has_Inf.Inf 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.

source
theorem exists_between_of_forall_le {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} (sne : s.nonempty) (tne : t.nonempty) (hst : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x ≤ 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.

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

The supremum of a singleton is the element of the singleton

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

The infimum of a singleton is the element of the singleton

source
@[simp]
theorem cSup_pair {α : Type u_1} [conditionally_complete_lattice α] (a b : α) :
has_Sup.Sup {a, b} = a ⊔ b
source
@[simp]
theorem cInf_pair {α : Type u_1} [conditionally_complete_lattice α] (a b : α) :
has_Inf.Inf {a, b} = a ⊓ b
source
theorem cInf_le_cSup {α : Type u_1} [conditionally_complete_lattice α] {s : set α} (hb : bdd_below s) (ha : bdd_above s) (ne : s.nonempty) :
has_Inf.Inf s ≤ has_Sup.Sup s

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

source
theorem cSup_union {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} (hs : bdd_above s) (sne : s.nonempty) (ht : bdd_above t) (tne : t.nonempty) :
has_Sup.Sup (s ∪ t) = has_Sup.Sup s ⊔ has_Sup.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.

source
theorem cInf_union {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} (hs : bdd_below s) (sne : s.nonempty) (ht : bdd_below t) (tne : t.nonempty) :
has_Inf.Inf (s ∪ t) = has_Inf.Inf s ⊓ has_Inf.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.

source
theorem cSup_inter_le {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} (hs : bdd_above s) (ht : bdd_above t) (hst : (s ∩ t).nonempty) :
has_Sup.Sup (s ∩ t) ≤ has_Sup.Sup s ⊓ has_Sup.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.

source
theorem le_cInf_inter {α : Type u_1} [conditionally_complete_lattice α] {s t : set α} :
bdd_below s → bdd_below t → (s ∩ t).nonempty → has_Inf.Inf s ⊔ has_Inf.Inf t ≤ has_Inf.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.

source
theorem cSup_insert {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (hs : bdd_above s) (sne : s.nonempty) :
has_Sup.Sup (has_insert.insert a s) = a ⊔ has_Sup.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.

source
theorem cInf_insert {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {a : α} (hs : bdd_below s) (sne : s.nonempty) :
has_Inf.Inf (has_insert.insert a s) = a ⊓ has_Inf.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.

source
@[simp]
theorem cInf_Icc {α : Type u_1} [conditionally_complete_lattice α] {a b : α} (h : a ≤ b) :
has_Inf.Inf (set.Icc a b) = a
source
@[simp]
theorem cInf_Ici {α : Type u_1} [conditionally_complete_lattice α] {a : α} :
has_Inf.Inf (set.Ici a) = a
source
@[simp]
theorem cInf_Ico {α : Type u_1} [conditionally_complete_lattice α] {a b : α} (h : a < b) :
has_Inf.Inf (set.Ico a b) = a
source
@[simp]
theorem cInf_Ioc {α : Type u_1} [conditionally_complete_lattice α] {a b : α} [densely_ordered α] (h : a < b) :
has_Inf.Inf (set.Ioc a b) = a
source
@[simp]
theorem cInf_Ioi {α : Type u_1} [conditionally_complete_lattice α] {a : α} [no_max_order α] [densely_ordered α] :
has_Inf.Inf (set.Ioi a) = a
source
@[simp]
theorem cInf_Ioo {α : Type u_1} [conditionally_complete_lattice α] {a b : α} [densely_ordered α] (h : a < b) :
has_Inf.Inf (set.Ioo a b) = a
source
@[simp]
theorem cSup_Icc {α : Type u_1} [conditionally_complete_lattice α] {a b : α} (h : a ≤ b) :
has_Sup.Sup (set.Icc a b) = b
source
@[simp]
theorem cSup_Ico {α : Type u_1} [conditionally_complete_lattice α] {a b : α} [densely_ordered α] (h : a < b) :
has_Sup.Sup (set.Ico a b) = b
source
@[simp]
theorem cSup_Iic {α : Type u_1} [conditionally_complete_lattice α] {a : α} :
has_Sup.Sup (set.Iic a) = a
source
@[simp]
theorem cSup_Iio {α : Type u_1} [conditionally_complete_lattice α] {a : α} [no_min_order α] [densely_ordered α] :
has_Sup.Sup (set.Iio a) = a
source
@[simp]
theorem cSup_Ioc {α : Type u_1} [conditionally_complete_lattice α] {a b : α} (h : a < b) :
has_Sup.Sup (set.Ioc a b) = b
source
@[simp]
theorem cSup_Ioo {α : Type u_1} [conditionally_complete_lattice α] {a b : α} [densely_ordered α] (h : a < b) :
has_Sup.Sup (set.Ioo a b) = b
source
theorem csupr_le {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] [nonempty ι] {f : ι → α} {c : α} (H : ∀ (x : ι), f x ≤ c) :
supr f ≤ c

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

source
theorem le_csupr {α : Type u_1} {ι : Sort u_4} [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

source
theorem le_csupr_of_le {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] {a : α} {f : ι → α} (H : bdd_above (set.range f)) (c : ι) (h : a ≤ f c) :
a ≤ supr f
source
theorem csupr_mono {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] {f g : ι → α} (B : bdd_above (set.range g)) (H : ∀ (x : ι), f x ≤ g x) :
supr f ≤ supr g

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

source
theorem le_csupr_set {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] {f : β → α} {s : set β} (H : bdd_above (f '' s)) {c : β} (hc : c ∈ s) :
f c ≤ ⨆ (i : ↥s), f ↑i
source
theorem cinfi_mono {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] {f g : ι → α} (B : bdd_below (set.range f)) (H : ∀ (x : ι), f x ≤ g x) :
infi f ≤ infi g

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

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

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

source
theorem cinfi_le {α : Type u_1} {ι : Sort u_4} [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

source
theorem cinfi_le_of_le {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] {a : α} {f : ι → α} (H : bdd_below (set.range f)) (c : ι) (h : f c ≤ a) :
infi f ≤ a
source
theorem cinfi_set_le {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] {f : β → α} {s : set β} (H : bdd_below (f '' s)) {c : β} (hc : c ∈ s) :
(⨅ (i : ↥s), f ↑i) ≤ f c
source
@[simp]
theorem csupr_const {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] [hι : nonempty ι] {a : α} :
(⨆ (b : ι), a) = a
source
@[simp]
theorem cinfi_const {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] [hι : nonempty ι] {a : α} :
(⨅ (b : ι), a) = a
source
@[simp]
theorem supr_unique {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] [unique ι] {s : ι → α} :
(⨆ (i : ι), s i) = s inhabited.default
source
@[simp]
theorem infi_unique {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] [unique ι] {s : ι → α} :
(⨅ (i : ι), s i) = s inhabited.default
source
@[simp]
theorem csupr_pos {α : Type u_1} [conditionally_complete_lattice α] {p : Prop} {f : p → α} (hp : p) :
(⨆ (h : p), f h) = f hp
source
@[simp]
theorem cinfi_pos {α : Type u_1} [conditionally_complete_lattice α] {p : Prop} {f : p → α} (hp : p) :
(⨅ (h : p), f h) = f hp
source
theorem csupr_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] {b : α} [nonempty ι] {f : ι → α} (h₁ : ∀ (i : ι), f i ≤ b) (h₂ : ∀ (w : α), w < b → (∃ (i : ι), w < f i)) :
(⨆ (i : ι), f i) = b

Introduction rule to prove that b is the supremum of f: it suffices to check that b is larger than f i for all i, and that this is not the case of any w<b. See supr_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.

source
theorem cinfi_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} {ι : Sort u_4} [conditionally_complete_lattice α] {b : α} [nonempty ι] {f : ι → α} (h₁ : ∀ (i : ι), b ≤ f i) (h₂ : ∀ (w : α), b < w → (∃ (i : ι), f i < w)) :
(⨅ (i : ι), f i) = b

Introduction rule to prove that b is the infimum of f: it suffices to check that b is smaller than f i for all i, and that this is not the case of any w>b. See infi_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.

source
theorem monotone.csupr_mem_Inter_Icc_of_antitone {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [semilattice_sup β] {f g : β → α} (hf : monotone f) (hg : antitone g) (h : f ≤ g) :
(⨆ (n : β), f n) ∈ ⋂ (n : β), set.Icc (f n) (g n)

Nested intervals lemma: if f is a monotone sequence, g is an antitone sequence, and f n ≤ g n for all n, then ⨆ n, f n belongs to all the intervals [f n, g n].

source
theorem csupr_mem_Inter_Icc_of_antitone_Icc {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [semilattice_sup β] {f g : β → α} (h : antitone (λ (n : β), set.Icc (f n) (g n))) (h' : ∀ (n : β), f n ≤ g n) :
(⨆ (n : β), f n) ∈ ⋂ (n : β), set.Icc (f n) (g n)

Nested intervals lemma: if [f n, g n] is an antitone sequence of nonempty closed intervals, then ⨆ n, f n belongs to all the intervals [f n, g n].

source
theorem cSup_eq_of_is_forall_le_of_forall_le_imp_ge {α : Type u_1} [conditionally_complete_lattice α] {s : set α} {b : α} (hs : s.nonempty) (h_is_ub : ∀ (a : α), a ∈ s → a ≤ b) (h_b_le_ub : ∀ (ub : α), (∀ (a : α), a ∈ s → a ≤ ub) → b ≤ ub) :
has_Sup.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'.
source
@[protected, instance]
def pi.conditionally_complete_lattice {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), conditionally_complete_lattice (α i)] :
conditionally_complete_lattice (Π (i : ι), α i)
Equations
source
theorem exists_lt_of_lt_cSup {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} {b : α} (hs : s.nonempty) (hb : b < has_Sup.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.

source
theorem exists_lt_of_lt_csupr {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order α] {b : α} [nonempty ι] {f : ι → α} (h : 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.

source
theorem exists_lt_of_cInf_lt {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} {b : α} (hs : s.nonempty) (hb : has_Inf.Inf 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.

source
theorem exists_lt_of_cinfi_lt {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order α] {a : α} [nonempty ι] {f : ι → α} (h : 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.

source
theorem Inf_eq_argmin_on {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} [is_well_order α has_lt.lt] (hs : s.nonempty) :
has_Inf.Inf s = function.argmin_on id is_well_founded.wf s hs
source
theorem is_least_Inf {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} [is_well_order α has_lt.lt] (hs : s.nonempty) :
is_least s (has_Inf.Inf s)
source
theorem le_cInf_iff' {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} {b : α} [is_well_order α has_lt.lt] (hs : s.nonempty) :
b ≤ has_Inf.Inf s ↔ b ∈ lower_bounds s
source
theorem Inf_mem {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} [is_well_order α has_lt.lt] (hs : s.nonempty) :
has_Inf.Inf s ∈ s
source
theorem infi_mem {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order α] [is_well_order α has_lt.lt] [nonempty ι] (f : ι → α) :
infi f ∈ set.range f
source
theorem monotone_on.map_Inf {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} [is_well_order α has_lt.lt] {β : Type u_2} [conditionally_complete_lattice β] {f : α → β} (hf : monotone_on f s) (hs : s.nonempty) :
f (has_Inf.Inf s) = has_Inf.Inf (f '' s)
source
theorem monotone.map_Inf {α : Type u_1} [conditionally_complete_linear_order α] {s : set α} [is_well_order α has_lt.lt] {β : Type u_2} [conditionally_complete_lattice β] {f : α → β} (hf : monotone f) (hs : s.nonempty) :
f (has_Inf.Inf s) = has_Inf.Inf (f '' s)

Lemmas about a conditionally complete linear order with bottom element #

In this case we have Sup ∅ = ⊥, so we can drop some nonempty/set.nonempty assumptions.

source
@[simp]
theorem cSup_empty {α : Type u_1} [conditionally_complete_linear_order_bot α] :
has_Sup.Sup ∅ = ⊥
source
@[simp]
theorem csupr_of_empty {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order_bot α] [is_empty ι] (f : ι → α) :
(⨆ (i : ι), f i) = ⊥
source
@[simp]
theorem csupr_false {α : Type u_1} [conditionally_complete_linear_order_bot α] (f : false → α) :
(⨆ (i : false), f i) = ⊥
source
@[simp]
theorem cInf_univ {α : Type u_1} [conditionally_complete_linear_order_bot α] :
has_Inf.Inf set.univ = ⊥
source
theorem is_lub_cSup' {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} (hs : bdd_above s) :
is_lub s (has_Sup.Sup s)
source
theorem cSup_le_iff' {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} (hs : bdd_above s) {a : α} :
has_Sup.Sup s ≤ a ↔ ∀ (x : α), x ∈ s → x ≤ a
source
theorem cSup_le' {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} {a : α} (h : a ∈ upper_bounds s) :
has_Sup.Sup s ≤ a
source
theorem le_cSup_iff' {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} {a : α} (h : bdd_above s) :
a ≤ has_Sup.Sup s ↔ ∀ (b : α), b ∈ upper_bounds s → a ≤ b
source
theorem le_csupr_iff' {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order_bot α] {s : ι → α} {a : α} (h : bdd_above (set.range s)) :
a ≤ supr s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b
source
theorem le_cInf_iff'' {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} {a : α} (ne : s.nonempty) :
a ≤ has_Inf.Inf s ↔ ∀ (b : α), b ∈ s → a ≤ b
source
theorem le_cinfi_iff' {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order_bot α] [nonempty ι] {f : ι → α} {a : α} :
a ≤ infi f ↔ ∀ (i : ι), a ≤ f i
source
theorem cInf_le' {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} {a : α} (h : a ∈ s) :
has_Inf.Inf s ≤ a
source
theorem cinfi_le' {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order_bot α] (f : ι → α) (i : ι) :
infi f ≤ f i
source
theorem exists_lt_of_lt_cSup' {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} {a : α} (h : a < has_Sup.Sup s) :
∃ (b : α) (H : b ∈ s), a < b
source
theorem csupr_le_iff' {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order_bot α] {f : ι → α} (h : bdd_above (set.range f)) {a : α} :
(⨆ (i : ι), f i) ≤ a ↔ ∀ (i : ι), f i ≤ a
source
theorem csupr_le' {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order_bot α] {f : ι → α} {a : α} (h : ∀ (i : ι), f i ≤ a) :
(⨆ (i : ι), f i) ≤ a
source
theorem exists_lt_of_lt_csupr' {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order_bot α] {f : ι → α} {a : α} (h : a < ⨆ (i : ι), f i) :
∃ (i : ι), a < f i
source
theorem csupr_mono' {α : Type u_1} {ι : Sort u_4} [conditionally_complete_linear_order_bot α] {ι' : Sort u_2} {f : ι → α} {g : ι' → α} (hg : bdd_above (set.range g)) (h : ∀ (i : ι), ∃ (i' : ι'), f i ≤ g i') :
supr f ≤ supr g
source
theorem cInf_le_cInf' {α : Type u_1} [conditionally_complete_linear_order_bot α] {s t : set α} (h₁ : t.nonempty) (h₂ : t ⊆ s) :
has_Inf.Inf s ≤ has_Inf.Inf t
source
theorem with_top.is_lub_Sup' {β : Type u_1} [conditionally_complete_lattice β] {s : set (with_top β)} (hs : s.nonempty) :
is_lub s (has_Sup.Sup s)

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

source
theorem with_top.is_lub_Sup {α : Type u_1} [conditionally_complete_linear_order_bot α] (s : set (with_top α)) :
is_lub s (has_Sup.Sup s)
source
theorem with_top.is_glb_Inf' {β : Type u_1} [conditionally_complete_lattice β] {s : set (with_top β)} (hs : bdd_below s) :
is_glb s (has_Inf.Inf s)

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

source
theorem with_top.is_glb_Inf {α : Type u_1} [conditionally_complete_linear_order_bot α] (s : set (with_top α)) :
is_glb s (has_Inf.Inf s)
source
@[protected, instance]
noncomputable def with_top.complete_linear_order {α : Type u_1} [conditionally_complete_linear_order_bot α] :
complete_linear_order (with_top α)
Equations
source
@[norm_cast]
theorem with_top.coe_Sup {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} (hb : bdd_above s) :
↑(has_Sup.Sup s) = ⨆ (a : α) (H : a ∈ s), ↑a

A version of with_top.coe_Sup' with a more convenient but less general statement.

source
@[norm_cast]
theorem with_top.coe_Inf {α : Type u_1} [conditionally_complete_linear_order_bot α] {s : set α} (hs : s.nonempty) :
↑(has_Inf.Inf s) = ⨅ (a : α) (H : a ∈ s), ↑a

A version of with_top.coe_Inf' with a more convenient but less general statement.

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

source
theorem monotone.le_cSup_image {α : Type u_1} {β : Type u_2} [preorder α] [conditionally_complete_lattice β] {f : α → β} (h_mono : monotone f) {s : set α} {c : α} (hcs : c ∈ s) (h_bdd : bdd_above s) :
f c ≤ has_Sup.Sup (f '' s)
source
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 : α} (hB : B ∈ upper_bounds s) :
has_Sup.Sup (f '' s) ≤ f B
source
theorem monotone.cInf_image_le {α : Type u_1} {β : Type u_2} [preorder α] [conditionally_complete_lattice β] {f : α → β} (h_mono : monotone f) {s : set α} {c : α} (hcs : c ∈ s) (h_bdd : bdd_below s) :
has_Inf.Inf (f '' s) ≤ f c
source
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 : α} (hB : B ∈ lower_bounds s) :
f B ≤ has_Inf.Inf (f '' s)
source
theorem galois_connection.l_cSup {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [conditionally_complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set α} (hne : s.nonempty) (hbdd : bdd_above s) :
l (has_Sup.Sup s) = ⨆ (x : ↥s), l ↑x
source
theorem galois_connection.l_cSup' {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [conditionally_complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set α} (hne : s.nonempty) (hbdd : bdd_above s) :
l (has_Sup.Sup s) = has_Sup.Sup (l '' s)
source
theorem galois_connection.l_csupr {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [nonempty ι] {l : α → β} {u : β → α} (gc : galois_connection l u) {f : ι → α} (hf : bdd_above (set.range f)) :
l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
source
theorem galois_connection.l_csupr_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set γ} {f : γ → α} (hf : bdd_above (f '' s)) (hne : s.nonempty) :
l (⨆ (i : ↥s), f ↑i) = ⨆ (i : ↥s), l (f ↑i)
source
theorem galois_connection.u_cInf {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [conditionally_complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set β} (hne : s.nonempty) (hbdd : bdd_below s) :
u (has_Inf.Inf s) = ⨅ (x : ↥s), u ↑x
source
theorem galois_connection.u_cInf' {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [conditionally_complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set β} (hne : s.nonempty) (hbdd : bdd_below s) :
u (has_Inf.Inf s) = has_Inf.Inf (u '' s)
source
theorem galois_connection.u_cinfi {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [nonempty ι] {l : α → β} {u : β → α} (gc : galois_connection l u) {f : ι → β} (hf : bdd_below (set.range f)) :
u (⨅ (i : ι), f i) = ⨅ (i : ι), u (f i)
source
theorem galois_connection.u_cinfi_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] {l : α → β} {u : β → α} (gc : galois_connection l u) {s : set γ} {f : γ → β} (hf : bdd_below (f '' s)) (hne : s.nonempty) :
u (⨅ (i : ↥s), f ↑i) = ⨅ (i : ↥s), u (f ↑i)
source
theorem order_iso.map_cSup {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [conditionally_complete_lattice β] (e : α ≃o β) {s : set α} (hne : s.nonempty) (hbdd : bdd_above s) :
⇑e (has_Sup.Sup s) = ⨆ (x : ↥s), ⇑e ↑x
source
theorem order_iso.map_cSup' {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [conditionally_complete_lattice β] (e : α ≃o β) {s : set α} (hne : s.nonempty) (hbdd : bdd_above s) :
⇑e (has_Sup.Sup s) = has_Sup.Sup (⇑e '' s)
source
theorem order_iso.map_csupr {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [nonempty ι] (e : α ≃o β) {f : ι → α} (hf : bdd_above (set.range f)) :
⇑e (⨆ (i : ι), f i) = ⨆ (i : ι), ⇑e (f i)
source
theorem order_iso.map_csupr_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] (e : α ≃o β) {s : set γ} {f : γ → α} (hf : bdd_above (f '' s)) (hne : s.nonempty) :
⇑e (⨆ (i : ↥s), f ↑i) = ⨆ (i : ↥s), ⇑e (f ↑i)
source
theorem order_iso.map_cInf {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [conditionally_complete_lattice β] (e : α ≃o β) {s : set α} (hne : s.nonempty) (hbdd : bdd_below s) :
⇑e (has_Inf.Inf s) = ⨅ (x : ↥s), ⇑e ↑x
source
theorem order_iso.map_cInf' {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [conditionally_complete_lattice β] (e : α ≃o β) {s : set α} (hne : s.nonempty) (hbdd : bdd_below s) :
⇑e (has_Inf.Inf s) = has_Inf.Inf (⇑e '' s)
source
theorem order_iso.map_cinfi {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [nonempty ι] (e : α ≃o β) {f : ι → α} (hf : bdd_below (set.range f)) :
⇑e (⨅ (i : ι), f i) = ⨅ (i : ι), ⇑e (f i)
source
theorem order_iso.map_cinfi_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] (e : α ≃o β) {s : set γ} {f : γ → α} (hf : bdd_below (f '' s)) (hne : s.nonempty) :
⇑e (⨅ (i : ↥s), f ↑i) = ⨅ (i : ↥s), ⇑e (f ↑i)

Supremum/infimum of set.image2 #

A collection of lemmas showing what happens to the suprema/infima of s and t when mapped under a binary function whose partial evaluations are lower/upper adjoints of Galois connections.

source
theorem cSup_image2_eq_cSup_cSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [conditionally_complete_lattice γ] {s : set α} {t : set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), galois_connection (l a) (u₂ a)) (hs₀ : s.nonempty) (hs₁ : bdd_above s) (ht₀ : t.nonempty) (ht₁ : bdd_above t) :
has_Sup.Sup (set.image2 l s t) = l (has_Sup.Sup s) (has_Sup.Sup t)
source
theorem cSup_image2_eq_cSup_cInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [conditionally_complete_lattice γ] {s : set α} {t : set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), galois_connection (l a ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ u₂ a)) :
s.nonempty → bdd_above s → t.nonempty → bdd_below t → has_Sup.Sup (set.image2 l s t) = l (has_Sup.Sup s) (has_Inf.Inf t)
source
theorem cSup_image2_eq_cInf_cSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [conditionally_complete_lattice γ] {s : set α} {t : set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (function.swap l b ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ u₁ b)) (h₂ : ∀ (a : α), galois_connection (l a) (u₂ a)) :
s.nonempty → bdd_below s → t.nonempty → bdd_above t → has_Sup.Sup (set.image2 l s t) = l (has_Inf.Inf s) (has_Sup.Sup t)
source
theorem cSup_image2_eq_cInf_cInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [conditionally_complete_lattice γ] {s : set α} {t : set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (function.swap l b ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ u₁ b)) (h₂ : ∀ (a : α), galois_connection (l a ∘ ⇑order_dual.of_dual) (⇑order_dual.to_dual ∘ u₂ a)) :
s.nonempty → bdd_below s → t.nonempty → bdd_below t → has_Sup.Sup (set.image2 l s t) = l (has_Inf.Inf s) (has_Inf.Inf t)
source
theorem cInf_image2_eq_cInf_cInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [conditionally_complete_lattice γ] {s : set α} {t : set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (l₁ b) (function.swap u b)) (h₂ : ∀ (a : α), galois_connection (l₂ a) (u a)) :
s.nonempty → bdd_below s → t.nonempty → bdd_below t → has_Inf.Inf (set.image2 u s t) = u (has_Inf.Inf s) (has_Inf.Inf t)
source
theorem cInf_image2_eq_cInf_cSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [conditionally_complete_lattice γ] {s : set α} {t : set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (l₁ b) (function.swap u b)) (h₂ : ∀ (a : α), galois_connection (⇑order_dual.to_dual ∘ l₂ a) (u a ∘ ⇑order_dual.of_dual)) :
s.nonempty → bdd_below s → t.nonempty → bdd_above t → has_Inf.Inf (set.image2 u s t) = u (has_Inf.Inf s) (has_Sup.Sup t)
source
theorem cInf_image2_eq_cSup_cInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [conditionally_complete_lattice γ] {s : set α} {t : set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (⇑order_dual.to_dual ∘ l₁ b) (function.swap u b ∘ ⇑order_dual.of_dual)) (h₂ : ∀ (a : α), galois_connection (l₂ a) (u a)) :
s.nonempty → bdd_above s → t.nonempty → bdd_below t → has_Inf.Inf (set.image2 u s t) = u (has_Sup.Sup s) (has_Inf.Inf t)
source
theorem cInf_image2_eq_cSup_cSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [conditionally_complete_lattice α] [conditionally_complete_lattice β] [conditionally_complete_lattice γ] {s : set α} {t : set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), galois_connection (⇑order_dual.to_dual ∘ l₁ b) (function.swap u b ∘ ⇑order_dual.of_dual)) (h₂ : ∀ (a : α), galois_connection (⇑order_dual.to_dual ∘ l₂ a) (u a ∘ ⇑order_dual.of_dual)) :
s.nonempty → bdd_above s → t.nonempty → bdd_above t → has_Inf.Inf (set.image2 u s t) = u (has_Sup.Sup s) (has_Sup.Sup t)

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 α) and with_bot (with_top α) naturally inherit 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 linear order.

source
@[protected, instance]
noncomputable def with_top.conditionally_complete_lattice {α : Type u_1} [conditionally_complete_lattice α] :
conditionally_complete_lattice (with_top α)

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

Equations
source
@[protected, instance]
noncomputable def with_bot.conditionally_complete_lattice {α : Type u_1} [conditionally_complete_lattice α] :
conditionally_complete_lattice (with_bot α)

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

Equations
source
@[protected, instance]
noncomputable def with_top.with_bot.complete_lattice {α : Type u_1} [conditionally_complete_lattice α] :
complete_lattice (with_top (with_bot α))
Equations
source
@[protected, instance]
noncomputable def with_top.with_bot.complete_linear_order {α : Type u_1} [conditionally_complete_linear_order α] :
complete_linear_order (with_top (with_bot α))
Equations
source
@[protected, instance]
noncomputable def with_bot.with_top.complete_lattice {α : Type u_1} [conditionally_complete_lattice α] :
complete_lattice (with_bot (with_top α))
Equations
source
@[protected, instance]
noncomputable def with_bot.with_top.complete_linear_order {α : Type u_1} [conditionally_complete_linear_order α] :
complete_linear_order (with_bot (with_top α))
Equations
source
theorem with_top.supr_coe_eq_top {ι : Sort u_1} {α : Type u_2} [conditionally_complete_linear_order_bot α] (f : ι → α) :
(⨆ (x : ι), ↑(f x)) = ⊤ ↔ ¬bdd_above (set.range f)
source
theorem with_top.supr_coe_lt_top {ι : Sort u_1} {α : Type u_2} [conditionally_complete_linear_order_bot α] (f : ι → α) :
(⨆ (x : ι), ↑(f x)) < ⊤ ↔ bdd_above (set.range f)