Theory of complete lattices

Main definitions

• sSup and sInf are the supremum and the infimum of a set;
• iSup (f : ι → α) and iInf (f : ι → α) are indexed supremum and infimum of a function, defined as sSup and sInf of the range of this function;
• class CompleteLattice: a bounded lattice such that sSup s is always the least upper boundary of s and sInf s is always the greatest lower boundary of s;
• class CompleteLinearOrder: a linear ordered complete lattice.

Naming conventions

In lemma names,

• sSup is called sSup
• sInf is called sInf
• ⨆ i, s i is called iSup
• ⨅ i, s i is called iInf
• ⨆ i j, s i j is called iSup₂. This is an iSup inside an iSup.
• ⨅ i j, s i j is called iInf₂. This is an iInf inside an iInf.
• ⨆ i ∈ s, t i is called biSup for "bounded iSup". This is the special case of iSup₂ where j : i ∈ s.
• ⨅ i ∈ s, t i is called biInf for "bounded iInf". This is the special case of iInf₂ where j : i ∈ s.

Notation

• ⨆ i, f i : iSup f, the supremum of the range of f;
• ⨅ i, f i : iInf f, the infimum of the range of f.

class SupSet (α : Type u_9) : Type u_9

• sSup : Set α → α

  Supremum of a set

Class for the sSup operator

class InfSet (α : Type u_9) : Type u_9

• sInf : Set α → α

  Infimum of a set

Class for the sInf operator

def iSup {α : Type u_1} [SupSet α] {ι : Sort u_9} (s : ι → α) : α

Indexed supremum

def iInf {α : Type u_1} [InfSet α] {ι : Sort u_9} (s : ι → α) : α

Indexed infimum

instance infSet_to_nonempty (α : Type u_9) [InfSet α] : Nonempty α

instance supSet_to_nonempty (α : Type u_9) [SupSet α] : Nonempty α

def «term⨆_,_» : Lean.ParserDescr

Indexed supremum.

def «term⨆_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

def «term⨅_,_» : Lean.ParserDescr

Indexed infimum.

def «term⨅_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

instance OrderDual.supSet (α : Type u_9) [InfSet α] : SupSet αᵒᵈ

instance OrderDual.infSet (α : Type u_9) [SupSet α] : InfSet αᵒᵈ

class CompleteSemilatticeSup (α : Type u_9) extends PartialOrder , SupSet : Type u_9

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• sSup : Set α → α
• le_sSup : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → a ≤ sSup s_1

  Any element of a set is less than the set supremum.

• sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → b ≤ a) → sSup s_1 ≤ a

  Any upper bound is more than the set supremum.

Note that we rarely use CompleteSemilatticeSup (in fact, any such object is always a CompleteLattice, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.

theorem le_sSup {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : a ∈ s → a ≤ sSup s

theorem sSup_le {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : (∀ (b : α), b ∈ s → b ≤ a) → sSup s ≤ a

theorem isLUB_sSup {α : Type u_1} [CompleteSemilatticeSup α] (s : Set α) : IsLUB s (sSup s)

theorem IsLUB.sSup_eq {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} (h : IsLUB s a) : sSup s = a

theorem le_sSup_of_le {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} {b : α} (hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s

theorem sSup_le_sSup {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {t : Set α} (h : s ⊆ t) : sSup s ≤ sSup t

@[simp]

theorem sSup_le_iff {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : sSup s ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a

theorem le_sSup_iff {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : a ≤ sSup s ↔ ∀ (b : α), b ∈ upperBounds s → a ≤ b

theorem le_iSup_iff {α : Type u_1} {ι : Sort u_5} [CompleteSemilatticeSup α] {a : α} {s : ι → α} : a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

theorem sSup_le_sSup_of_forall_exists_le {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {t : Set α} (h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ x ≤ y) : sSup s ≤ sSup t

theorem sSup_singleton {α : Type u_1} [CompleteSemilatticeSup α] {a : α} : sSup {a} = a

class CompleteSemilatticeInf (α : Type u_9) extends PartialOrder , InfSet : Type u_9

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• sInf : Set α → α
• sInf_le : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → sInf s_1 ≤ a

  Any element of a set is more than the set infimum.

• le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → a ≤ b) → a ≤ sInf s_1

  Any lower bound is less than the set infimum.

Note that we rarely use CompleteSemilatticeInf (in fact, any such object is always a CompleteLattice, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.

theorem sInf_le {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : a ∈ s → sInf s ≤ a

theorem le_sInf {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : (∀ (b : α), b ∈ s → a ≤ b) → a ≤ sInf s

theorem isGLB_sInf {α : Type u_1} [CompleteSemilatticeInf α] (s : Set α) : IsGLB s (sInf s)

theorem IsGLB.sInf_eq {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} (h : IsGLB s a) : sInf s = a

theorem sInf_le_of_le {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} {b : α} (hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a

theorem sInf_le_sInf {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {t : Set α} (h : s ⊆ t) : sInf t ≤ sInf s

@[simp]

theorem le_sInf_iff {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : a ≤ sInf s ↔ ∀ (b : α), b ∈ s → a ≤ b

theorem sInf_le_iff {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : sInf s ≤ a ↔ ∀ (b : α), b ∈ lowerBounds s → b ≤ a

theorem iInf_le_iff {α : Type u_1} {ι : Sort u_5} [CompleteSemilatticeInf α] {a : α} {s : ι → α} : iInf s ≤ a ↔ ∀ (b : α), (∀ (i : ι), b ≤ s i) → b ≤ a

theorem sInf_le_sInf_of_forall_exists_le {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {t : Set α} (h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x) : sInf t ≤ sInf s

theorem sInf_singleton {α : Type u_1} [CompleteSemilatticeInf α] {a : α} : sInf {a} = a

class CompleteLattice (α : Type u_9) extends Lattice , SupSet , InfSet , Top , Bot : Type u_9

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• 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 : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
• sSup : Set α → α
• le_sSup : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → a ≤ sSup s_1

  Any element of a set is less than the set supremum.

• sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → b ≤ a) → sSup s_1 ≤ a

  Any upper bound is more than the set supremum.

• sInf : Set α → α
• sInf_le : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → sInf s_1 ≤ a

  Any element of a set is more than the set infimum.

• le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → a ≤ b) → a ≤ sInf s_1

  Any lower bound is less than the set infimum.

• top : α
• bot : α
• le_top : ∀ (x : α), x ≤ ⊤

  Any element is less than the top one.

• bot_le : ∀ (x : α), ⊥ ≤ x

  Any element is more than the bottom one.

A complete lattice is a bounded lattice which has suprema and infima for every subset.

instance CompleteLattice.toBoundedOrder {α : Type u_1} [h : CompleteLattice α] : BoundedOrder α

def completeLatticeOfInf (α : Type u_9) [H1 : PartialOrder α] [H2 : InfSet α] (isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)) : CompleteLattice α

Create a CompleteLattice from a PartialOrder and InfSet that returns the greatest lower bound of a set. 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 CompleteLattice instance as

instance : CompleteLattice my_T :=
  { inf := better_inf,
    le_inf := ...,
    inf_le_right := ...,
    inf_le_left := ...
    -- don't care to fix sup, sSup, bot, top
    ..completeLatticeOfInf my_T _ }

def completeLatticeOfCompleteSemilatticeInf (α : Type u_9) [CompleteSemilatticeInf α] : CompleteLattice α

Any CompleteSemilatticeInf is in fact a CompleteLattice.

Note that this construction has bad definitional properties: see the doc-string on completeLatticeOfInf.

def completeLatticeOfSup (α : Type u_9) [H1 : PartialOrder α] [H2 : SupSet α] (isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)) : CompleteLattice α

Create a CompleteLattice from a PartialOrder and SupSet that returns the least upper bound of a set. 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 CompleteLattice instance as

instance : CompleteLattice my_T :=
  { inf := better_inf,
    le_inf := ...,
    inf_le_right := ...,
    inf_le_left := ...
    -- don't care to fix sup, sInf, bot, top
    ..completeLatticeOfSup my_T _ }

def completeLatticeOfCompleteSemilatticeSup (α : Type u_9) [CompleteSemilatticeSup α] : CompleteLattice α

Any CompleteSemilatticeSup is in fact a CompleteLattice.

Note that this construction has bad definitional properties: see the doc-string on completeLatticeOfSup.

class CompleteLinearOrder (α : Type u_9) extends CompleteLattice : Type u_9

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• 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 : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
• sSup : Set α → α
• le_sSup : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → a ≤ sSup s_1
• sSup_le : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → b ≤ a) → sSup s_1 ≤ a
• sInf : Set α → α
• sInf_le : ∀ (s_1 : Set α) (a : α), a ∈ s_1 → sInf s_1 ≤ a
• le_sInf : ∀ (s_1 : Set α) (a : α), (∀ (b : α), b ∈ s_1 → a ≤ b) → a ≤ sInf s_1
• top : α
• bot : α
• le_top : ∀ (x : α), x ≤ ⊤
• bot_le : ∀ (x : α), ⊥ ≤ x
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

  A linear order is total.

• decidableLE : DecidableRel fun x x_1 => x ≤ x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq : DecidableEq α

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun x x_1 => x < x_1

  In a linearly ordered type, we assume the order relations are all decidable.

A complete linear order is a linear order whose lattice structure is complete.

instance CompleteLinearOrder.toLinearOrder {α : Type u_1} [i : CompleteLinearOrder α] : LinearOrder α

instance OrderDual.completeLattice (α : Type u_1) [CompleteLattice α] : CompleteLattice αᵒᵈ

instance OrderDual.instCompleteLinearOrderOrderDual (α : Type u_1) [CompleteLinearOrder α] : CompleteLinearOrder αᵒᵈ

@[simp]

theorem toDual_sSup {α : Type u_1} [CompleteLattice α] (s : Set α) : ↑OrderDual.toDual (sSup s) = sInf (↑OrderDual.ofDual ⁻¹' s)

@[simp]

theorem toDual_sInf {α : Type u_1} [CompleteLattice α] (s : Set α) : ↑OrderDual.toDual (sInf s) = sSup (↑OrderDual.ofDual ⁻¹' s)

@[simp]

theorem ofDual_sSup {α : Type u_1} [CompleteLattice α] (s : Set αᵒᵈ) : ↑OrderDual.ofDual (sSup s) = sInf (↑OrderDual.toDual ⁻¹' s)

@[simp]

theorem ofDual_sInf {α : Type u_1} [CompleteLattice α] (s : Set αᵒᵈ) : ↑OrderDual.ofDual (sInf s) = sSup (↑OrderDual.toDual ⁻¹' s)

@[simp]

theorem toDual_iSup {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → α) : ↑OrderDual.toDual (⨆ (i : ι), f i) = ⨅ (i : ι), ↑OrderDual.toDual (f i)

@[simp]

theorem toDual_iInf {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → α) : ↑OrderDual.toDual (⨅ (i : ι), f i) = ⨆ (i : ι), ↑OrderDual.toDual (f i)

@[simp]

theorem ofDual_iSup {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → αᵒᵈ) : ↑OrderDual.ofDual (⨆ (i : ι), f i) = ⨅ (i : ι), ↑OrderDual.ofDual (f i)

@[simp]

theorem ofDual_iInf {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → αᵒᵈ) : ↑OrderDual.ofDual (⨅ (i : ι), f i) = ⨆ (i : ι), ↑OrderDual.ofDual (f i)

theorem sInf_le_sSup {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : Set.Nonempty s) : sInf s ≤ sSup s

theorem sSup_union {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} : sSup (s ∪ t) = sSup s ⊔ sSup t

theorem sInf_union {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} : sInf (s ∪ t) = sInf s ⊓ sInf t

theorem sSup_inter_le {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} : sSup (s ∩ t) ≤ sSup s ⊓ sSup t

theorem le_sInf_inter {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} : sInf s ⊔ sInf t ≤ sInf (s ∩ t)

@[simp]

theorem sSup_empty {α : Type u_1} [CompleteLattice α] : sSup ∅ = ⊥

@[simp]

theorem sInf_empty {α : Type u_1} [CompleteLattice α] : sInf ∅ = ⊤

@[simp]

theorem sSup_univ {α : Type u_1} [CompleteLattice α] : sSup Set.univ = ⊤

@[simp]

theorem sInf_univ {α : Type u_1} [CompleteLattice α] : sInf Set.univ = ⊥

@[simp]

theorem sSup_insert {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : sSup (insert a s) = a ⊔ sSup s

@[simp]

theorem sInf_insert {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : sInf (insert a s) = a ⊓ sInf s

theorem sSup_le_sSup_of_subset_insert_bot {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} (h : s ⊆ insert ⊥ t) : sSup s ≤ sSup t

theorem sInf_le_sInf_of_subset_insert_top {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} (h : s ⊆ insert ⊤ t) : sInf t ≤ sInf s

@[simp]

theorem sSup_diff_singleton_bot {α : Type u_1} [CompleteLattice α] (s : Set α) : sSup (s \ {⊥}) = sSup s

@[simp]

theorem sInf_diff_singleton_top {α : Type u_1} [CompleteLattice α] (s : Set α) : sInf (s \ {⊤}) = sInf s

theorem sSup_pair {α : Type u_1} [CompleteLattice α] {a : α} {b : α} : sSup {a, b} = a ⊔ b

theorem sInf_pair {α : Type u_1} [CompleteLattice α] {a : α} {b : α} : sInf {a, b} = a ⊓ b

@[simp]

theorem sSup_eq_bot {α : Type u_1} [CompleteLattice α] {s : Set α} : sSup s = ⊥ ↔ ∀ (a : α), a ∈ s → a = ⊥

@[simp]

theorem sInf_eq_top {α : Type u_1} [CompleteLattice α] {s : Set α} : sInf s = ⊤ ↔ ∀ (a : α), a ∈ s → a = ⊤

theorem eq_singleton_bot_of_sSup_eq_bot_of_nonempty {α : Type u_1} [CompleteLattice α] {s : Set α} (h_sup : sSup s = ⊥) (hne : Set.Nonempty s) : s = {⊥}

theorem eq_singleton_top_of_sInf_eq_top_of_nonempty {α : Type u_1} [CompleteLattice α] {s : Set α} : sInf s = ⊤ → Set.Nonempty s → s = {⊤}

theorem sSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [CompleteLattice α] {s : Set α} {b : α} (h₁ : ∀ (a : α), a ∈ s → a ≤ b) (h₂ : ∀ (w : α), w < b → ∃ a, a ∈ s ∧ w < a) : sSup 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 csSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in conditionally complete lattices.

theorem sInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [CompleteLattice α] {s : Set α} {b : α} : (∀ (a : α), a ∈ s → b ≤ a) → (∀ (w : α), b < w → ∃ a, a ∈ s ∧ a < w) → sInf 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 csInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in conditionally complete lattices.

theorem lt_sSup_iff {α : Type u_1} [CompleteLinearOrder α] {s : Set α} {b : α} : b < sSup s ↔ ∃ a, a ∈ s ∧ b < a

theorem sInf_lt_iff {α : Type u_1} [CompleteLinearOrder α] {s : Set α} {b : α} : sInf s < b ↔ ∃ a, a ∈ s ∧ a < b

theorem sSup_eq_top {α : Type u_1} [CompleteLinearOrder α] {s : Set α} : sSup s = ⊤ ↔ ∀ (b : α), b < ⊤ → ∃ a, a ∈ s ∧ b < a

theorem sInf_eq_bot {α : Type u_1} [CompleteLinearOrder α] {s : Set α} : sInf s = ⊥ ↔ ∀ (b : α), b > ⊥ → ∃ a, a ∈ s ∧ a < b

theorem lt_iSup_iff {α : Type u_1} {ι : Sort u_5} [CompleteLinearOrder α] {a : α} {f : ι → α} : a < iSup f ↔ ∃ i, a < f i

theorem iInf_lt_iff {α : Type u_1} {ι : Sort u_5} [CompleteLinearOrder α] {a : α} {f : ι → α} : iInf f < a ↔ ∃ i, f i < a

theorem sSup_range {α : Type u_1} {ι : Sort u_5} [SupSet α] {f : ι → α} : sSup (Set.range f) = iSup f

theorem sSup_eq_iSup' {α : Type u_1} [SupSet α] (s : Set α) : sSup s = ⨆ (a : ↑s), ↑a

theorem iSup_congr {α : Type u_1} {ι : Sort u_5} [SupSet α] {f : ι → α} {g : ι → α} (h : ∀ (i : ι), f i = g i) : ⨆ (i : ι), f i = ⨆ (i : ι), g i

theorem Function.Surjective.iSup_comp {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [SupSet α] {f : ι → ι'} (hf : Function.Surjective f) (g : ι' → α) : ⨆ (x : ι), g (f x) = ⨆ (y : ι'), g y

theorem Equiv.iSup_comp {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [SupSet α] {g : ι' → α} (e : ι ≃ ι') : ⨆ (x : ι), g (↑e x) = ⨆ (y : ι'), g y

theorem Function.Surjective.iSup_congr {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [SupSet α] {f : ι → α} {g : ι' → α} (h : ι → ι') (h1 : Function.Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) : ⨆ (x : ι), f x = ⨆ (y : ι'), g y

theorem Equiv.iSup_congr {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [SupSet α] {f : ι → α} {g : ι' → α} (e : ι ≃ ι') (h : ∀ (x : ι), g (↑e x) = f x) : ⨆ (x : ι), f x = ⨆ (y : ι'), g y

theorem iSup_congr_Prop {α : Type u_1} [SupSet α] {p : Prop} {q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q) (f : ∀ (x : q), f₁ (Iff.mpr pq x) = f₂ x) : iSup f₁ = iSup f₂

theorem iSup_plift_up {α : Type u_1} {ι : Sort u_5} [SupSet α] (f : PLift ι → α) : ⨆ (i : ι), f { down := i } = ⨆ (i : PLift ι), f i

theorem iSup_plift_down {α : Type u_1} {ι : Sort u_5} [SupSet α] (f : ι → α) : ⨆ (i : PLift ι), f i.down = ⨆ (i : ι), f i

theorem iSup_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [SupSet α] (g : β → α) (f : ι → β) : ⨆ (b : ↑(Set.range f)), g ↑b = ⨆ (i : ι), g (f i)

theorem sSup_image' {α : Type u_1} {β : Type u_2} [SupSet α] {s : Set β} {f : β → α} : sSup (f '' s) = ⨆ (a : ↑s), f ↑a

theorem sInf_range {α : Type u_1} {ι : Sort u_5} [InfSet α] {f : ι → α} : sInf (Set.range f) = iInf f

theorem sInf_eq_iInf' {α : Type u_1} [InfSet α] (s : Set α) : sInf s = ⨅ (a : ↑s), ↑a

theorem iInf_congr {α : Type u_1} {ι : Sort u_5} [InfSet α] {f : ι → α} {g : ι → α} (h : ∀ (i : ι), f i = g i) : ⨅ (i : ι), f i = ⨅ (i : ι), g i

theorem Function.Surjective.iInf_comp {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [InfSet α] {f : ι → ι'} (hf : Function.Surjective f) (g : ι' → α) : ⨅ (x : ι), g (f x) = ⨅ (y : ι'), g y

theorem Equiv.iInf_comp {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [InfSet α] {g : ι' → α} (e : ι ≃ ι') : ⨅ (x : ι), g (↑e x) = ⨅ (y : ι'), g y

theorem Function.Surjective.iInf_congr {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [InfSet α] {f : ι → α} {g : ι' → α} (h : ι → ι') (h1 : Function.Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) : ⨅ (x : ι), f x = ⨅ (y : ι'), g y

theorem Equiv.iInf_congr {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [InfSet α] {f : ι → α} {g : ι' → α} (e : ι ≃ ι') (h : ∀ (x : ι), g (↑e x) = f x) : ⨅ (x : ι), f x = ⨅ (y : ι'), g y

theorem iInf_congr_Prop {α : Type u_1} [InfSet α] {p : Prop} {q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q) (f : ∀ (x : q), f₁ (Iff.mpr pq x) = f₂ x) : iInf f₁ = iInf f₂

theorem iInf_plift_up {α : Type u_1} {ι : Sort u_5} [InfSet α] (f : PLift ι → α) : ⨅ (i : ι), f { down := i } = ⨅ (i : PLift ι), f i

theorem iInf_plift_down {α : Type u_1} {ι : Sort u_5} [InfSet α] (f : ι → α) : ⨅ (i : PLift ι), f i.down = ⨅ (i : ι), f i

theorem iInf_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [InfSet α] (g : β → α) (f : ι → β) : ⨅ (b : ↑(Set.range f)), g ↑b = ⨅ (i : ι), g (f i)

theorem sInf_image' {α : Type u_1} {β : Type u_2} [InfSet α] {s : Set β} {f : β → α} : sInf (f '' s) = ⨅ (a : ↑s), f ↑a

theorem le_iSup {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → α) (i : ι) : f i ≤ iSup f

theorem iInf_le {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → α) (i : ι) : iInf f ≤ f i

theorem le_iSup' {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → α) (i : ι) : f i ≤ iSup f

theorem iInf_le' {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → α) (i : ι) : iInf f ≤ f i

theorem isLUB_iSup {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} : IsLUB (Set.range f) (⨆ (j : ι), f j)

theorem isGLB_iInf {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} : IsGLB (Set.range f) (⨅ (j : ι), f j)

theorem IsLUB.iSup_eq {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {a : α} (h : IsLUB (Set.range f) a) : ⨆ (j : ι), f j = a

theorem IsGLB.iInf_eq {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {a : α} (h : IsGLB (Set.range f) a) : ⨅ (j : ι), f j = a

theorem le_iSup_of_le {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {a : α} (i : ι) (h : a ≤ f i) : a ≤ iSup f

theorem iInf_le_of_le {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {a : α} (i : ι) (h : f i ≤ a) : iInf f ≤ a

theorem le_iSup₂ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {f : (i : ι) → κ i → α} (i : ι) (j : κ i) : f i j ≤ ⨆ (i : ι) (j : κ i), f i j

theorem iInf₂_le {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {f : (i : ι) → κ i → α} (i : ι) (j : κ i) : ⨅ (i : ι) (j : κ i), f i j ≤ f i j

theorem le_iSup₂_of_le {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (i : ι) (j : κ i) (h : a ≤ f i j) : a ≤ ⨆ (i : ι) (j : κ i), f i j

theorem iInf₂_le_of_le {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (i : ι) (j : κ i) (h : f i j ≤ a) : ⨅ (i : ι) (j : κ i), f i j ≤ a

theorem iSup_le {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {a : α} (h : ∀ (i : ι), f i ≤ a) : iSup f ≤ a

theorem le_iInf {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {a : α} (h : ∀ (i : ι), a ≤ f i) : a ≤ iInf f

theorem iSup₂_le {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), f i j ≤ a) : ⨆ (i : ι) (j : κ i), f i j ≤ a

theorem le_iInf₂ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), a ≤ f i j) : a ≤ ⨅ (i : ι) (j : κ i), f i j

theorem iSup₂_le_iSup {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (κ : ι → Sort u_9) (f : ι → α) : ⨆ (i : ι) (x : κ i), f i ≤ ⨆ (i : ι), f i

theorem iInf_le_iInf₂ {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (κ : ι → Sort u_9) (f : ι → α) : ⨅ (i : ι), f i ≤ ⨅ (i : ι) (x : κ i), f i

theorem iSup_mono {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {g : ι → α} (h : ∀ (i : ι), f i ≤ g i) : iSup f ≤ iSup g

theorem iInf_mono {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {g : ι → α} (h : ∀ (i : ι), f i ≤ g i) : iInf f ≤ iInf g

theorem iSup₂_mono {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {f : (i : ι) → κ i → α} {g : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), f i j ≤ g i j) : ⨆ (i : ι) (j : κ i), f i j ≤ ⨆ (i : ι) (j : κ i), g i j

theorem iInf₂_mono {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {f : (i : ι) → κ i → α} {g : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), f i j ≤ g i j) : ⨅ (i : ι) (j : κ i), f i j ≤ ⨅ (i : ι) (j : κ i), g i j

theorem iSup_mono' {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [CompleteLattice α] {f : ι → α} {g : ι' → α} (h : ∀ (i : ι), ∃ i', f i ≤ g i') : iSup f ≤ iSup g

theorem iInf_mono' {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [CompleteLattice α] {f : ι → α} {g : ι' → α} (h : ∀ (i' : ι'), ∃ i, f i ≤ g i') : iInf f ≤ iInf g

theorem iSup₂_mono' {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {κ : ι → Sort u_7} {κ' : ι' → Sort u_8} [CompleteLattice α] {f : (i : ι) → κ i → α} {g : (i' : ι') → κ' i' → α} (h : ∀ (i : ι) (j : κ i), ∃ i' j', f i j ≤ g i' j') : ⨆ (i : ι) (j : κ i), f i j ≤ ⨆ (i : ι') (j : κ' i), g i j

theorem iInf₂_mono' {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {κ : ι → Sort u_7} {κ' : ι' → Sort u_8} [CompleteLattice α] {f : (i : ι) → κ i → α} {g : (i' : ι') → κ' i' → α} (h : ∀ (i : ι') (j : κ' i), ∃ i' j', f i' j' ≤ g i j) : ⨅ (i : ι) (j : κ i), f i j ≤ ⨅ (i : ι') (j : κ' i), g i j

theorem iSup_const_mono {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [CompleteLattice α] {a : α} (h : ι → ι') : ⨆ (x : ι), a ≤ ⨆ (x : ι'), a

theorem iInf_const_mono {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [CompleteLattice α] {a : α} (h : ι' → ι) : ⨅ (x : ι), a ≤ ⨅ (x : ι'), a

theorem iSup_iInf_le_iInf_iSup {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [CompleteLattice α] (f : ι → ι' → α) : ⨆ (i : ι), ⨅ (j : ι'), f i j ≤ ⨅ (j : ι'), ⨆ (i : ι), f i j

theorem biSup_mono {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {p : ι → Prop} {q : ι → Prop} (hpq : (i : ι) → p i → q i) : ⨆ (i : ι) (x : p i), f i ≤ ⨆ (i : ι) (x : q i), f i

theorem biInf_mono {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {p : ι → Prop} {q : ι → Prop} (hpq : (i : ι) → p i → q i) : ⨅ (i : ι) (x : q i), f i ≤ ⨅ (i : ι) (x : p i), f i

@[simp]

theorem iSup_le_iff {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {a : α} : iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a

@[simp]

theorem le_iInf_iff {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {a : α} : a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i

theorem iSup₂_le_iff {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} : ⨆ (i : ι) (j : κ i), f i j ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a

theorem le_iInf₂_iff {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} : a ≤ ⨅ (i : ι) (j : κ i), f i j ↔ ∀ (i : ι) (j : κ i), a ≤ f i j

theorem iSup_lt_iff {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {a : α} : iSup f < a ↔ ∃ b, b < a ∧ ∀ (i : ι), f i ≤ b

theorem lt_iInf_iff {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {a : α} : a < iInf f ↔ ∃ b, a < b ∧ ∀ (i : ι), b ≤ f i

theorem sSup_eq_iSup {α : Type u_1} [CompleteLattice α] {s : Set α} : sSup s = ⨆ (a : α) (_ : a ∈ s), a

theorem sInf_eq_iInf {α : Type u_1} [CompleteLattice α] {s : Set α} : sInf s = ⨅ (a : α) (_ : a ∈ s), a

theorem Monotone.le_map_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] {s : ι → α} [CompleteLattice β] {f : α → β} (hf : Monotone f) : ⨆ (i : ι), f (s i) ≤ f (iSup s)

theorem Antitone.le_map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] {s : ι → α} [CompleteLattice β] {f : α → β} (hf : Antitone f) : ⨆ (i : ι), f (s i) ≤ f (iInf s)

theorem Monotone.le_map_iSup₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : Monotone f) (s : (i : ι) → κ i → α) : ⨆ (i : ι) (j : κ i), f (s i j) ≤ f (⨆ (i : ι) (j : κ i), s i j)

theorem Antitone.le_map_iInf₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : Antitone f) (s : (i : ι) → κ i → α) : ⨆ (i : ι) (j : κ i), f (s i j) ≤ f (⨅ (i : ι) (j : κ i), s i j)

theorem Monotone.le_map_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) : ⨆ (a : α) (_ : a ∈ s), f a ≤ f (sSup s)

theorem Antitone.le_map_sInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) : ⨆ (a : α) (_ : a ∈ s), f a ≤ f (sInf s)

theorem OrderIso.map_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (x : ι → α) : ↑f (⨆ (i : ι), x i) = ⨆ (i : ι), ↑f (x i)

theorem OrderIso.map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (x : ι → α) : ↑f (⨅ (i : ι), x i) = ⨅ (i : ι), ↑f (x i)

theorem OrderIso.map_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) : ↑f (sSup s) = ⨆ (a : α) (_ : a ∈ s), ↑f a

theorem OrderIso.map_sInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) : ↑f (sInf s) = ⨅ (a : α) (_ : a ∈ s), ↑f a

theorem iSup_comp_le {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {ι' : Sort u_9} (f : ι' → α) (g : ι → ι') : ⨆ (x : ι), f (g x) ≤ ⨆ (y : ι'), f y

theorem le_iInf_comp {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {ι' : Sort u_9} (f : ι' → α) (g : ι → ι') : ⨅ (y : ι'), f y ≤ ⨅ (x : ι), f (g x)

theorem Monotone.iSup_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] [Preorder β] {f : β → α} (hf : Monotone f) {s : ι → β} (hs : ∀ (x : β), ∃ i, x ≤ s i) : ⨆ (x : ι), f (s x) = ⨆ (y : β), f y

theorem Monotone.iInf_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] [Preorder β] {f : β → α} (hf : Monotone f) {s : ι → β} (hs : ∀ (x : β), ∃ i, s i ≤ x) : ⨅ (x : ι), f (s x) = ⨅ (y : β), f y

theorem Antitone.map_iSup_le {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] {s : ι → α} [CompleteLattice β] {f : α → β} (hf : Antitone f) : f (iSup s) ≤ ⨅ (i : ι), f (s i)

theorem Monotone.map_iInf_le {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] {s : ι → α} [CompleteLattice β] {f : α → β} (hf : Monotone f) : f (iInf s) ≤ ⨅ (i : ι), f (s i)

theorem Antitone.map_iSup₂_le {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : Antitone f) (s : (i : ι) → κ i → α) : f (⨆ (i : ι) (j : κ i), s i j) ≤ ⨅ (i : ι) (j : κ i), f (s i j)

theorem Monotone.map_iInf₂_le {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : Monotone f) (s : (i : ι) → κ i → α) : f (⨅ (i : ι) (j : κ i), s i j) ≤ ⨅ (i : ι) (j : κ i), f (s i j)

theorem Antitone.map_sSup_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) : f (sSup s) ≤ ⨅ (a : α) (_ : a ∈ s), f a

theorem Monotone.map_sInf_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) : f (sInf s) ≤ ⨅ (a : α) (_ : a ∈ s), f a

theorem iSup_const_le {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {a : α} : ⨆ (x : ι), a ≤ a

theorem le_iInf_const {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {a : α} : a ≤ ⨅ (x : ι), a

theorem iSup_const {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {a : α} [Nonempty ι] : ⨆ (x : ι), a = a

theorem iInf_const {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {a : α} [Nonempty ι] : ⨅ (x : ι), a = a

@[simp]

theorem iSup_bot {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] : ⨆ (x : ι), ⊥ = ⊥

@[simp]

theorem iInf_top {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] : ⨅ (x : ι), ⊤ = ⊤

@[simp]

theorem iSup_eq_bot {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {s : ι → α} : iSup s = ⊥ ↔ ∀ (i : ι), s i = ⊥

@[simp]

theorem iInf_eq_top {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {s : ι → α} : iInf s = ⊤ ↔ ∀ (i : ι), s i = ⊤

theorem iSup₂_eq_bot {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {f : (i : ι) → κ i → α} : ⨆ (i : ι) (j : κ i), f i j = ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥

theorem iInf₂_eq_top {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [CompleteLattice α] {f : (i : ι) → κ i → α} : ⨅ (i : ι) (j : κ i), f i j = ⊤ ↔ ∀ (i : ι) (j : κ i), f i j = ⊤

@[simp]

theorem iSup_pos {α : Type u_1} [CompleteLattice α] {p : Prop} {f : p → α} (hp : p) : ⨆ (h : p), f h = f hp

@[simp]

theorem iInf_pos {α : Type u_1} [CompleteLattice α] {p : Prop} {f : p → α} (hp : p) : ⨅ (h : p), f h = f hp

@[simp]

theorem iSup_neg {α : Type u_1} [CompleteLattice α] {p : Prop} {f : p → α} (hp : ¬p) : ⨆ (h : p), f h = ⊥

@[simp]

theorem iInf_neg {α : Type u_1} [CompleteLattice α] {p : Prop} {f : p → α} (hp : ¬p) : ⨅ (h : p), f h = ⊤

theorem iSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {b : α} {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. See ciSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in conditionally complete lattices.

theorem iInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {b : α} : (∀ (i : ι), b ≤ f i) → (∀ (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 ciInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in conditionally complete lattices.

theorem iSup_eq_dif {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : p → α) : ⨆ (h : p), a h = if h : p then a h else ⊥

theorem iSup_eq_if {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : α) : ⨆ (x : p), a = if p then a else ⊥

theorem iInf_eq_dif {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : p → α) : ⨅ (h : p), a h = if h : p then a h else ⊤

theorem iInf_eq_if {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : α) : ⨅ (x : p), a = if p then a else ⊤

theorem iSup_comm {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [CompleteLattice α] {f : ι → ι' → α} : ⨆ (i : ι) (j : ι'), f i j = ⨆ (j : ι') (i : ι), f i j

theorem iInf_comm {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [CompleteLattice α] {f : ι → ι' → α} : ⨅ (i : ι) (j : ι'), f i j = ⨅ (j : ι') (i : ι), f i j

theorem iSup₂_comm {α : Type u_1} [CompleteLattice α] {ι₁ : Sort u_9} {ι₂ : Sort u_10} {κ₁ : ι₁ → Sort u_11} {κ₂ : ι₂ → Sort u_12} (f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α) : ⨆ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂ = ⨆ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂

theorem iInf₂_comm {α : Type u_1} [CompleteLattice α] {ι₁ : Sort u_9} {ι₂ : Sort u_10} {κ₁ : ι₁ → Sort u_11} {κ₂ : ι₂ → Sort u_12} (f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α) : ⨅ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂ = ⨅ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂

@[simp]

theorem iSup_iSup_eq_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → x = b → α} : ⨆ (x : β) (h : x = b), f x h = f b (_ : b = b)

@[simp]

theorem iInf_iInf_eq_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → x = b → α} : ⨅ (x : β) (h : x = b), f x h = f b (_ : b = b)

@[simp]

theorem iSup_iSup_eq_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → b = x → α} : ⨆ (x : β) (h : b = x), f x h = f b (_ : b = b)

@[simp]

theorem iInf_iInf_eq_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → b = x → α} : ⨅ (x : β) (h : b = x), f x h = f b (_ : b = b)

theorem iSup_subtype {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {p : ι → Prop} {f : Subtype p → α} : iSup f = ⨆ (i : ι) (h : p i), f { val := i, property := h }

theorem iInf_subtype {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {p : ι → Prop} {f : Subtype p → α} : iInf f = ⨅ (i : ι) (h : p i), f { val := i, property := h }

theorem iSup_subtype' {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} : ⨆ (i : ι) (h : p i), f i h = ⨆ (x : Subtype p), f (↑x) x.property

theorem iInf_subtype' {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} : ⨅ (i : ι) (h : p i), f i h = ⨅ (x : Subtype p), f (↑x) x.property

theorem iSup_subtype'' {α : Type u_1} [CompleteLattice α] {ι : Type u_9} (s : Set ι) (f : ι → α) : ⨆ (i : ↑s), f ↑i = ⨆ (t : ι) (_ : t ∈ s), f t

theorem iInf_subtype'' {α : Type u_1} [CompleteLattice α] {ι : Type u_9} (s : Set ι) (f : ι → α) : ⨅ (i : ↑s), f ↑i = ⨅ (t : ι) (_ : t ∈ s), f t

theorem biSup_const {α : Type u_1} [CompleteLattice α] {ι : Type u_9} {a : α} {s : Set ι} (hs : Set.Nonempty s) : ⨆ (i : ι) (_ : i ∈ s), a = a

theorem biInf_const {α : Type u_1} [CompleteLattice α] {ι : Type u_9} {a : α} {s : Set ι} (hs : Set.Nonempty s) : ⨅ (i : ι) (_ : i ∈ s), a = a

theorem iSup_sup_eq {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {g : ι → α} : ⨆ (x : ι), f x ⊔ g x = (⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x

theorem iInf_inf_eq {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {f : ι → α} {g : ι → α} : ⨅ (x : ι), f x ⊓ g x = (⨅ (x : ι), f x) ⊓ ⨅ (x : ι), g x

theorem iSup_sup {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α} : (⨆ (x : ι), f x) ⊔ a = ⨆ (x : ι), f x ⊔ a

theorem iInf_inf {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α} : (⨅ (x : ι), f x) ⊓ a = ⨅ (x : ι), f x ⊓ a

theorem sup_iSup {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α} : a ⊔ ⨆ (x : ι), f x = ⨆ (x : ι), a ⊔ f x

theorem inf_iInf {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α} : a ⊓ ⨅ (x : ι), f x = ⨅ (x : ι), a ⊓ f x

theorem biSup_sup {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} (h : ∃ i, p i) : (⨆ (i : ι) (h : p i), f i h) ⊔ a = ⨆ (i : ι) (h : p i), f i h ⊔ a

theorem sup_biSup {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} (h : ∃ i, p i) : a ⊔ ⨆ (i : ι) (h : p i), f i h = ⨆ (i : ι) (h : p i), a ⊔ f i h

theorem biInf_inf {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} (h : ∃ i, p i) : (⨅ (i : ι) (h : p i), f i h) ⊓ a = ⨅ (i : ι) (h : p i), f i h ⊓ a

theorem inf_biInf {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} (h : ∃ i, p i) : a ⊓ ⨅ (i : ι) (h : p i), f i h = ⨅ (i : ι) (h : p i), a ⊓ f i h

iSup and iInf under Prop

theorem iSup_false {α : Type u_1} [CompleteLattice α] {s : False → α} : iSup s = ⊥

theorem iInf_false {α : Type u_1} [CompleteLattice α] {s : False → α} : iInf s = ⊤

theorem iSup_true {α : Type u_1} [CompleteLattice α] {s : True → α} : iSup s = s trivial

theorem iInf_true {α : Type u_1} [CompleteLattice α] {s : True → α} : iInf s = s trivial

@[simp]

theorem iSup_exists {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {p : ι → Prop} {f : Exists p → α} : ⨆ (x : Exists p), f x = ⨆ (i : ι) (h : p i), f (_ : Exists p)

@[simp]

theorem iInf_exists {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] {p : ι → Prop} {f : Exists p → α} : ⨅ (x : Exists p), f x = ⨅ (i : ι) (h : p i), f (_ : Exists p)

theorem iSup_and {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : p ∧ q → α} : iSup s = ⨆ (h₁ : p) (h₂ : q), s (_ : p ∧ q)

theorem iInf_and {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : p ∧ q → α} : iInf s = ⨅ (h₁ : p) (h₂ : q), s (_ : p ∧ q)

theorem iSup_and' {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : p → q → α} : ⨆ (h₁ : p) (h₂ : q), s h₁ h₂ = ⨆ (h : p ∧ q), s h.left h.right

The symmetric case of iSup_and, useful for rewriting into a supremum over a conjunction

theorem iInf_and' {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : p → q → α} : ⨅ (h₁ : p) (h₂ : q), s h₁ h₂ = ⨅ (h : p ∧ q), s h.left h.right

The symmetric case of iInf_and, useful for rewriting into an infimum over a conjunction

theorem iSup_or {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : p ∨ q → α} : ⨆ (x : p ∨ q), s x = (⨆ (i : p), s (_ : p ∨ q)) ⊔ ⨆ (j : q), s (_ : p ∨ q)

theorem iInf_or {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : p ∨ q → α} : ⨅ (x : p ∨ q), s x = (⨅ (i : p), s (_ : p ∨ q)) ⊓ ⨅ (j : q), s (_ : p ∨ q)

theorem iSup_dite {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (p : ι → Prop) [DecidablePred p] (f : (i : ι) → p i → α) (g : (i : ι) → ¬p i → α) : (⨆ (i : ι), if h : p i then f i h else g i h) = (⨆ (i : ι) (h : p i), f i h) ⊔ ⨆ (i : ι) (h : ¬p i), g i h

theorem iInf_dite {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (p : ι → Prop) [DecidablePred p] (f : (i : ι) → p i → α) (g : (i : ι) → ¬p i → α) : (⨅ (i : ι), if h : p i then f i h else g i h) = (⨅ (i : ι) (h : p i), f i h) ⊓ ⨅ (i : ι) (h : ¬p i), g i h

theorem iSup_ite {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (p : ι → Prop) [DecidablePred p] (f : ι → α) (g : ι → α) : (⨆ (i : ι), if p i then f i else g i) = (⨆ (i : ι) (x : p i), f i) ⊔ ⨆ (i : ι) (_ : ¬p i), g i

theorem iInf_ite {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (p : ι → Prop) [DecidablePred p] (f : ι → α) (g : ι → α) : (⨅ (i : ι), if p i then f i else g i) = (⨅ (i : ι) (x : p i), f i) ⊓ ⨅ (i : ι) (_ : ¬p i), g i

theorem iSup_range {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] {g : β → α} {f : ι → β} : ⨆ (b : β) (_ : b ∈ Set.range f), g b = ⨆ (i : ι), g (f i)

theorem iInf_range {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] {g : β → α} {f : ι → β} : ⨅ (b : β) (_ : b ∈ Set.range f), g b = ⨅ (i : ι), g (f i)

theorem sSup_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : β → α} : sSup (f '' s) = ⨆ (a : β) (_ : a ∈ s), f a

theorem sInf_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : β → α} : sInf (f '' s) = ⨅ (a : β) (_ : a ∈ s), f a

theorem iSup_emptyset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} : ⨆ (x : β) (_ : x ∈ ∅), f x = ⊥

theorem iInf_emptyset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} : ⨅ (x : β) (_ : x ∈ ∅), f x = ⊤

theorem iSup_univ {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} : ⨆ (x : β) (_ : x ∈ Set.univ), f x = ⨆ (x : β), f x

theorem iInf_univ {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} : ⨅ (x : β) (_ : x ∈ Set.univ), f x = ⨅ (x : β), f x

theorem iSup_union {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s : Set β} {t : Set β} : ⨆ (x : β) (_ : x ∈ s ∪ t), f x = (⨆ (x : β) (_ : x ∈ s), f x) ⊔ ⨆ (x : β) (_ : x ∈ t), f x

theorem iInf_union {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s : Set β} {t : Set β} : ⨅ (x : β) (_ : x ∈ s ∪ t), f x = (⨅ (x : β) (_ : x ∈ s), f x) ⊓ ⨅ (x : β) (_ : x ∈ t), f x

theorem iSup_split {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (p : β → Prop) : ⨆ (i : β), f i = (⨆ (i : β) (x : p i), f i) ⊔ ⨆ (i : β) (_ : ¬p i), f i

theorem iInf_split {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (p : β → Prop) : ⨅ (i : β), f i = (⨅ (i : β) (x : p i), f i) ⊓ ⨅ (i : β) (_ : ¬p i), f i

theorem iSup_split_single {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (i₀ : β) : ⨆ (i : β), f i = f i₀ ⊔ ⨆ (i : β) (_ : i ≠ i₀), f i

theorem iInf_split_single {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) (i₀ : β) : ⨅ (i : β), f i = f i₀ ⊓ ⨅ (i : β) (_ : i ≠ i₀), f i

theorem iSup_le_iSup_of_subset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s : Set β} {t : Set β} : s ⊆ t → ⨆ (x : β) (_ : x ∈ s), f x ≤ ⨆ (x : β) (_ : x ∈ t), f x

theorem iInf_le_iInf_of_subset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s : Set β} {t : Set β} : s ⊆ t → ⨅ (x : β) (_ : x ∈ t), f x ≤ ⨅ (x : β) (_ : x ∈ s), f x

theorem iSup_insert {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s : Set β} {b : β} : ⨆ (x : β) (_ : x ∈ insert b s), f x = f b ⊔ ⨆ (x : β) (_ : x ∈ s), f x

theorem iInf_insert {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {s : Set β} {b : β} : ⨅ (x : β) (_ : x ∈ insert b s), f x = f b ⊓ ⨅ (x : β) (_ : x ∈ s), f x

theorem iSup_singleton {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {b : β} : ⨆ (x : β) (_ : x ∈ {b}), f x = f b

theorem iInf_singleton {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {b : β} : ⨅ (x : β) (_ : x ∈ {b}), f x = f b

theorem iSup_pair {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {a : β} {b : β} : ⨆ (x : β) (_ : x ∈ {a, b}), f x = f a ⊔ f b

theorem iInf_pair {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : β → α} {a : β} {b : β} : ⨅ (x : β) (_ : x ∈ {a, b}), f x = f a ⊓ f b

theorem iSup_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {γ : Type u_9} {f : β → γ} {g : γ → α} {t : Set β} : ⨆ (c : γ) (_ : c ∈ f '' t), g c = ⨆ (b : β) (_ : b ∈ t), g (f b)

theorem iInf_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {γ : Type u_9} {f : β → γ} {g : γ → α} {t : Set β} : ⨅ (c : γ) (_ : c ∈ f '' t), g c = ⨅ (b : β) (_ : b ∈ t), g (f b)

theorem iSup_extend_bot {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] {e : ι → β} (he : Function.Injective e) (f : ι → α) : ⨆ (j : β), Function.extend e f ⊥ j = ⨆ (i : ι), f i

theorem iInf_extend_top {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice α] {e : ι → β} (he : Function.Injective e) (f : ι → α) : ⨅ (j : β), Function.extend e f ⊤ j = iInf f

iSup and iInf under Type

theorem iSup_of_empty' {α : Type u_9} {ι : Sort u_10} [SupSet α] [IsEmpty ι] (f : ι → α) : iSup f = sSup ∅

theorem iInf_of_empty' {α : Type u_9} {ι : Sort u_10} [InfSet α] [IsEmpty ι] (f : ι → α) : iInf f = sInf ∅

theorem iSup_of_empty {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] [IsEmpty ι] (f : ι → α) : iSup f = ⊥

theorem iInf_of_empty {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] [IsEmpty ι] (f : ι → α) : iInf f = ⊤

theorem iSup_bool_eq {α : Type u_1} [CompleteLattice α] {f : Bool → α} : ⨆ (b : Bool), f b = f true ⊔ f false

theorem iInf_bool_eq {α : Type u_1} [CompleteLattice α] {f : Bool → α} : ⨅ (b : Bool), f b = f true ⊓ f false

theorem sup_eq_iSup {α : Type u_1} [CompleteLattice α] (x : α) (y : α) : x ⊔ y = ⨆ (b : Bool), bif b then x else y

theorem inf_eq_iInf {α : Type u_1} [CompleteLattice α] (x : α) (y : α) : x ⊓ y = ⨅ (b : Bool), bif b then x else y

theorem isGLB_biInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : β → α} : IsGLB (f '' s) (⨅ (x : β) (_ : x ∈ s), f x)

theorem isLUB_biSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : β → α} : IsLUB (f '' s) (⨆ (x : β) (_ : x ∈ s), f x)

theorem iSup_sigma {α : Type u_1} {β : Type u_2} [CompleteLattice α] {p : β → Type u_9} {f : Sigma p → α} : ⨆ (x : Sigma p), f x = ⨆ (i : β) (j : p i), f { fst := i, snd := j }

theorem iInf_sigma {α : Type u_1} {β : Type u_2} [CompleteLattice α] {p : β → Type u_9} {f : Sigma p → α} : ⨅ (x : Sigma p), f x = ⨅ (i : β) (j : p i), f { fst := i, snd := j }

theorem iSup_sigma' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {κ : β → Type u_9} (f : (i : β) → κ i → α) : ⨆ (i : β) (j : κ i), f i j = ⨆ (x : (i : β) × κ i), f x.fst x.snd

theorem iInf_sigma' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {κ : β → Type u_9} (f : (i : β) → κ i → α) : ⨅ (i : β) (j : κ i), f i j = ⨅ (x : (i : β) × κ i), f x.fst x.snd

theorem iSup_prod {α : Type u_1} {β : Type u_2} {γ : Type u_4} [CompleteLattice α] {f : β × γ → α} : ⨆ (x : β × γ), f x = ⨆ (i : β) (j : γ), f (i, j)

theorem iInf_prod {α : Type u_1} {β : Type u_2} {γ : Type u_4} [CompleteLattice α] {f : β × γ → α} : ⨅ (x : β × γ), f x = ⨅ (i : β) (j : γ), f (i, j)

theorem iSup_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_4} [CompleteLattice α] (f : β → γ → α) : ⨆ (i : β) (j : γ), f i j = ⨆ (x : β × γ), f x.fst x.snd

theorem iInf_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_4} [CompleteLattice α] (f : β → γ → α) : ⨅ (i : β) (j : γ), f i j = ⨅ (x : β × γ), f x.fst x.snd

theorem biSup_prod {α : Type u_1} {β : Type u_2} {γ : Type u_4} [CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ} : ⨆ (x : β × γ) (_ : x ∈ s ×ˢ t), f x = ⨆ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f (a, b)

theorem biInf_prod {α : Type u_1} {β : Type u_2} {γ : Type u_4} [CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ} : ⨅ (x : β × γ) (_ : x ∈ s ×ˢ t), f x = ⨅ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f (a, b)

theorem iSup_sum {α : Type u_1} {β : Type u_2} {γ : Type u_4} [CompleteLattice α] {f : β ⊕ γ → α} : ⨆ (x : β ⊕ γ), f x = (⨆ (i : β), f (Sum.inl i)) ⊔ ⨆ (j : γ), f (Sum.inr j)

theorem iInf_sum {α : Type u_1} {β : Type u_2} {γ : Type u_4} [CompleteLattice α] {f : β ⊕ γ → α} : ⨅ (x : β ⊕ γ), f x = (⨅ (i : β), f (Sum.inl i)) ⊓ ⨅ (j : γ), f (Sum.inr j)

theorem iSup_option {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : Option β → α) : ⨆ (o : Option β), f o = f none ⊔ ⨆ (b : β), f (some b)

theorem iInf_option {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : Option β → α) : ⨅ (o : Option β), f o = f none ⊓ ⨅ (b : β), f (some b)

theorem iSup_option_elim {α : Type u_1} {β : Type u_2} [CompleteLattice α] (a : α) (f : β → α) : ⨆ (o : Option β), Option.elim o a f = a ⊔ ⨆ (b : β), f b

A version of iSup_option useful for rewriting right-to-left.

theorem iInf_option_elim {α : Type u_1} {β : Type u_2} [CompleteLattice α] (a : α) (f : β → α) : ⨅ (o : Option β), Option.elim o a f = a ⊓ ⨅ (b : β), f b

A version of iInf_option useful for rewriting right-to-left.

theorem iSup_ne_bot_subtype {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → α) : ⨆ (i : { i // f i ≠ ⊥ }), f ↑i = ⨆ (i : ι), f i

When taking the supremum of f : ι → α, the elements of ι on which f gives ⊥ can be dropped, without changing the result.

theorem iInf_ne_top_subtype {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → α) : ⨅ (i : { i // f i ≠ ⊤ }), f ↑i = ⨅ (i : ι), f i

When taking the infimum of f : ι → α, the elements of ι on which f gives ⊤ can be dropped, without changing the result.

theorem sSup_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_4} [CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} : sSup (Set.image2 f s t) = ⨆ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f a b

theorem sInf_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_4} [CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} : sInf (Set.image2 f s t) = ⨅ (a : β) (_ : a ∈ s) (b : γ) (_ : b ∈ t), f a b

iSup and iInf under ℕ

theorem iSup_ge_eq_iSup_nat_add {α : Type u_1} [CompleteLattice α] (u : ℕ → α) (n : ℕ) : ⨆ (i : ℕ) (_ : i ≥ n), u i = ⨆ (i : ℕ), u (i + n)

theorem iInf_ge_eq_iInf_nat_add {α : Type u_1} [CompleteLattice α] (u : ℕ → α) (n : ℕ) : ⨅ (i : ℕ) (_ : i ≥ n), u i = ⨅ (i : ℕ), u (i + n)

theorem Monotone.iSup_nat_add {α : Type u_1} [CompleteLattice α] {f : ℕ → α} (hf : Monotone f) (k : ℕ) : ⨆ (n : ℕ), f (n + k) = ⨆ (n : ℕ), f n

theorem Antitone.iInf_nat_add {α : Type u_1} [CompleteLattice α] {f : ℕ → α} (hf : Antitone f) (k : ℕ) : ⨅ (n : ℕ), f (n + k) = ⨅ (n : ℕ), f n

theorem iSup_iInf_ge_nat_add {α : Type u_1} [CompleteLattice α] (f : ℕ → α) (k : ℕ) : ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f (i + k) = ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f i

theorem iInf_iSup_ge_nat_add {α : Type u_1} [CompleteLattice α] (f : ℕ → α) (k : ℕ) : ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), f (i + k) = ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), f i

theorem sup_iSup_nat_succ {α : Type u_1} [CompleteLattice α] (u : ℕ → α) : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ (i : ℕ), u i

theorem inf_iInf_nat_succ {α : Type u_1} [CompleteLattice α] (u : ℕ → α) : u 0 ⊓ ⨅ (i : ℕ), u (i + 1) = ⨅ (i : ℕ), u i

theorem iInf_nat_gt_zero_eq {α : Type u_1} [CompleteLattice α] (f : ℕ → α) : ⨅ (i : ℕ) (_ : i > 0), f i = ⨅ (i : ℕ), f (i + 1)

theorem iSup_nat_gt_zero_eq {α : Type u_1} [CompleteLattice α] (f : ℕ → α) : ⨆ (i : ℕ) (_ : i > 0), f i = ⨆ (i : ℕ), f (i + 1)

theorem iSup_eq_top {α : Type u_1} {ι : Sort u_5} [CompleteLinearOrder α] (f : ι → α) : iSup f = ⊤ ↔ ∀ (b : α), b < ⊤ → ∃ i, b < f i

theorem iInf_eq_bot {α : Type u_1} {ι : Sort u_5} [CompleteLinearOrder α] (f : ι → α) : iInf f = ⊥ ↔ ∀ (b : α), b > ⊥ → ∃ i, f i < b

Instances

instance Prop.completeLattice : CompleteLattice Prop

noncomputable instance Prop.completeLinearOrder : CompleteLinearOrder Prop

@[simp]

theorem sSup_Prop_eq {s : Set Prop} : sSup s = ∃ p, p ∈ s ∧ p

@[simp]

theorem sInf_Prop_eq {s : Set Prop} : sInf s = ∀ (p : Prop), p ∈ s → p

@[simp]

theorem iSup_Prop_eq {ι : Sort u_5} {p : ι → Prop} : ⨆ (i : ι), p i = ∃ i, p i

@[simp]

theorem iInf_Prop_eq {ι : Sort u_5} {p : ι → Prop} : ⨅ (i : ι), p i = ((i : ι) → p i)

instance Pi.supSet {α : Type u_9} {β : α → Type u_10} [(i : α) → SupSet (β i)] : SupSet ((i : α) → β i)

instance Pi.infSet {α : Type u_9} {β : α → Type u_10} [(i : α) → InfSet (β i)] : InfSet ((i : α) → β i)

instance Pi.completeLattice {α : Type u_9} {β : α → Type u_10} [(i : α) → CompleteLattice (β i)] : CompleteLattice ((i : α) → β i)

theorem sSup_apply {α : Type u_9} {β : α → Type u_10} [(i : α) → SupSet (β i)] {s : Set ((a : α) → β a)} {a : α} : sSup ((a : α) → β a) Pi.supSet s a = ⨆ (f : ↑s), ↑f a

theorem sInf_apply {α : Type u_9} {β : α → Type u_10} [(i : α) → InfSet (β i)] {s : Set ((a : α) → β a)} {a : α} : sInf ((a : α) → β a) Pi.infSet s a = ⨅ (f : ↑s), ↑f a

@[simp]

theorem iSup_apply {α : Type u_9} {β : α → Type u_10} {ι : Sort u_11} [(i : α) → SupSet (β i)] {f : ι → (a : α) → β a} {a : α} : iSup ((a : α) → β a) Pi.supSet ι (fun i => f i) a = ⨆ (i : ι), f i a

@[simp]

theorem iInf_apply {α : Type u_9} {β : α → Type u_10} {ι : Sort u_11} [(i : α) → InfSet (β i)] {f : ι → (a : α) → β a} {a : α} : iInf ((a : α) → β a) Pi.infSet ι (fun i => f i) a = ⨅ (i : ι), f i a

theorem unary_relation_sSup_iff {α : Type u_9} (s : Set (α → Prop)) {a : α} : sSup s a ↔ ∃ r, r ∈ s ∧ r a

theorem unary_relation_sInf_iff {α : Type u_9} (s : Set (α → Prop)) {a : α} : sInf s a ↔ (r : α → Prop) → r ∈ s → r a

theorem binary_relation_sSup_iff {α : Type u_9} {β : Type u_10} (s : Set (α → β → Prop)) {a : α} {b : β} : sSup s a b ↔ ∃ r, r ∈ s ∧ r a b

theorem binary_relation_sInf_iff {α : Type u_9} {β : Type u_10} (s : Set (α → β → Prop)) {a : α} {b : β} : sInf s a b ↔ (r : α → β → Prop) → r ∈ s → r a b

theorem monotone_sSup_of_monotone {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (α → β)} (m_s : ∀ (f : α → β), f ∈ s → Monotone f) : Monotone (sSup s)

theorem monotone_sInf_of_monotone {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (α → β)} (m_s : ∀ (f : α → β), f ∈ s → Monotone f) : Monotone (sInf s)

instance Prod.supSet (α : Type u_1) (β : Type u_2) [SupSet α] [SupSet β] : SupSet (α × β)

instance Prod.infSet (α : Type u_1) (β : Type u_2) [InfSet α] [InfSet β] : InfSet (α × β)

theorem Prod.fst_sInf {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).fst = sInf (Prod.fst '' s)

theorem Prod.snd_sInf {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).snd = sInf (Prod.snd '' s)

theorem Prod.swap_sInf {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) : Prod.swap (sInf s) = sInf (Prod.swap '' s)

theorem Prod.fst_sSup {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).fst = sSup (Prod.fst '' s)

theorem Prod.snd_sSup {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).snd = sSup (Prod.snd '' s)

theorem Prod.swap_sSup {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] (s : Set (α × β)) : Prod.swap (sSup s) = sSup (Prod.swap '' s)

theorem Prod.fst_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [InfSet α] [InfSet β] (f : ι → α × β) : (iInf f).fst = ⨅ (i : ι), (f i).fst

theorem Prod.snd_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [InfSet α] [InfSet β] (f : ι → α × β) : (iInf f).snd = ⨅ (i : ι), (f i).snd

theorem Prod.swap_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [InfSet α] [InfSet β] (f : ι → α × β) : Prod.swap (iInf f) = ⨅ (i : ι), Prod.swap (f i)

theorem Prod.iInf_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [InfSet α] [InfSet β] (f : ι → α) (g : ι → β) : ⨅ (i : ι), (f i, g i) = (⨅ (i : ι), f i, ⨅ (i : ι), g i)

theorem Prod.fst_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).fst = ⨆ (i : ι), (f i).fst

theorem Prod.snd_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).snd = ⨆ (i : ι), (f i).snd

theorem Prod.swap_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [SupSet α] [SupSet β] (f : ι → α × β) : Prod.swap (iSup f) = ⨆ (i : ι), Prod.swap (f i)

theorem Prod.iSup_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [SupSet α] [SupSet β] (f : ι → α) (g : ι → β) : ⨆ (i : ι), (f i, g i) = (⨆ (i : ι), f i, ⨆ (i : ι), g i)

instance Prod.completeLattice (α : Type u_1) (β : Type u_2) [CompleteLattice α] [CompleteLattice β] : CompleteLattice (α × β)

theorem sInf_prod {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] {s : Set α} {t : Set β} (hs : Set.Nonempty s) (ht : Set.Nonempty t) : sInf (s ×ˢ t) = (sInf s, sInf t)

theorem sSup_prod {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] {s : Set α} {t : Set β} (hs : Set.Nonempty s) (ht : Set.Nonempty t) : sSup (s ×ˢ t) = (sSup s, sSup t)

theorem sup_sInf_le_iInf_sup {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : a ⊔ sInf s ≤ ⨅ (b : α) (_ : b ∈ s), a ⊔ b

This is a weaker version of sup_sInf_eq

theorem iSup_inf_le_inf_sSup {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : ⨆ (b : α) (_ : b ∈ s), a ⊓ b ≤ a ⊓ sSup s

This is a weaker version of inf_sSup_eq

theorem sInf_sup_le_iInf_sup {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : sInf s ⊔ a ≤ ⨅ (b : α) (_ : b ∈ s), b ⊔ a

This is a weaker version of sInf_sup_eq

theorem iSup_inf_le_sSup_inf {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : ⨆ (b : α) (_ : b ∈ s), b ⊓ a ≤ sSup s ⊓ a

This is a weaker version of sSup_inf_eq

theorem le_iSup_inf_iSup {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → α) (g : ι → α) : ⨆ (i : ι), f i ⊓ g i ≤ (⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i

theorem iInf_sup_iInf_le {α : Type u_1} {ι : Sort u_5} [CompleteLattice α] (f : ι → α) (g : ι → α) : (⨅ (i : ι), f i) ⊔ ⨅ (i : ι), g i ≤ ⨅ (i : ι), f i ⊔ g i

theorem disjoint_sSup_left {α : Type u_1} [CompleteLattice α] {a : Set α} {b : α} (d : Disjoint (sSup a) b) {i : α} (hi : i ∈ a) : Disjoint i b

theorem disjoint_sSup_right {α : Type u_1} [CompleteLattice α] {a : Set α} {b : α} (d : Disjoint b (sSup a)) {i : α} (hi : i ∈ a) : Disjoint b i

@[reducible]

def Function.Injective.completeLattice {α : Type u_1} {β : Type u_2} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [CompleteLattice β] (f : α → β) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ (a : α) (_ : a ∈ s), f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ (a : α) (_ : a ∈ s), f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : CompleteLattice α

Pullback a CompleteLattice along an injection.

instance ULift.supSet {α : Type u_1} [SupSet α] : SupSet (ULift.{v, u_1} α)

theorem ULift.down_sSup {α : Type u_1} [SupSet α] (s : Set (ULift.{v, u_1} α)) : (sSup s).down = sSup (ULift.up ⁻¹' s)

theorem ULift.up_sSup {α : Type u_1} [SupSet α] (s : Set α) : { down := sSup s } = sSup (ULift.down ⁻¹' s)

instance ULift.infSet {α : Type u_1} [InfSet α] : InfSet (ULift.{v, u_1} α)

theorem ULift.down_sInf {α : Type u_1} [InfSet α] (s : Set (ULift.{v, u_1} α)) : (sInf s).down = sInf (ULift.up ⁻¹' s)

theorem ULift.up_sInf {α : Type u_1} [InfSet α] (s : Set α) : { down := sInf s } = sInf (ULift.down ⁻¹' s)

theorem ULift.down_iSup {α : Type u_1} {ι : Sort u_5} [SupSet α] (f : ι → ULift.{v, u_1} α) : (⨆ (i : ι), f i).down = ⨆ (i : ι), (f i).down

theorem ULift.up_iSup {α : Type u_1} {ι : Sort u_5} [SupSet α] (f : ι → α) : { down := ⨆ (i : ι), f i } = ⨆ (i : ι), { down := f i }

theorem ULift.down_iInf {α : Type u_1} {ι : Sort u_5} [InfSet α] (f : ι → ULift.{v, u_1} α) : (⨅ (i : ι), f i).down = ⨅ (i : ι), (f i).down

theorem ULift.up_iInf {α : Type u_1} {ι : Sort u_5} [InfSet α] (f : ι → α) : { down := ⨅ (i : ι), f i } = ⨅ (i : ι), { down := f i }

instance ULift.completeLattice {α : Type u_1} [CompleteLattice α] : CompleteLattice (ULift.{v, u_1} α)