Theory of complete lattices

Main definitions

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

Naming conventions

In lemma names,

• supₛ is called supₛ
• infₛ is called infₛ
• ⨆ i, s i⨆ i, s i is called supᵢ
• ⨅ i, s i⨅ i, s i is called infᵢ
• ⨆ i j, s i j⨆ i j, s i j is called supᵢ₂. This is a supᵢ inside a supᵢ.
• ⨅ i j, s i j⨅ i j, s i j is called infᵢ₂. This is an infᵢ inside an infᵢ.
• ⨆ i ∈ s, t i⨆ i ∈ s, t i∈ s, t i is called bsupᵢ for "bounded supᵢ". This is the special case of supᵢ₂ where j : i ∈ s∈ s.
• ⨅ i ∈ s, t i⨅ i ∈ s, t i∈ s, t i is called binfᵢ for "bounded infᵢ". This is the special case of infᵢ₂ where j : i ∈ s∈ s.

Notation

• ⨆ i, f i⨆ i, f i : supᵢ f, the supremum of the range of f;
• ⨅ i, f i⨅ i, f i : infᵢ f, the infimum of the range of f.

ink

class SupSet (α : Type u_1) : Type u_1

• Supremum of a set

  supₛ : Set α → α

class for the supₛ operator

ink

class InfSet (α : Type u_1) : Type u_1

• Infimum of a set

  infₛ : Set α → α

class for the infₛ operator

ink

def supᵢ {α : Type u_1} [inst : SupSet α] {ι : Sort u_2} (s : ι → α) : α

Indexed supremum

Equations

• supᵢ s = supₛ (Set.range s)

ink

def infᵢ {α : Type u_1} [inst : InfSet α] {ι : Sort u_2} (s : ι → α) : α

Indexed infimum

Equations

• infᵢ s = infₛ (Set.range s)

ink

instance infSet_to_nonempty (α : Type u_1) [inst : InfSet α] : Nonempty α

Equations

• infSet_to_nonempty = infSet_to_nonempty.proof_1

ink

instance supSet_to_nonempty (α : Type u_1) [inst : SupSet α] : Nonempty α

Equations

• supSet_to_nonempty = supSet_to_nonempty.proof_1

ink

def «⨆_,_» : Lean.ParserDescr

Indexed supremum.

Equations

• One or more equations did not get rendered due to their size.

ink

def supᵢ.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the indexed supremum notation.

Equations

• One or more equations did not get rendered due to their size.

ink

def «⨅_,_» : Lean.ParserDescr

Indexed infimum.

Equations

• One or more equations did not get rendered due to their size.

ink

def infᵢ.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the indexed infimum notation.

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• OrderDual.supSet α = { supₛ := infₛ }

ink

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

Equations

• OrderDual.infSet α = { infₛ := supₛ }

ink

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

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

  le_supₛ : ∀ (s : Set α) (a : α), a ∈ s → a ≤ supₛ s

• Any upper bound is more than the set supremum.

  supₛ_le : ∀ (s : Set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → supₛ s ≤ a

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.

ink

theorem le_supₛ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} : a ∈ s → a ≤ supₛ s

ink

theorem supₛ_le {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} : (∀ (b : α), b ∈ s → b ≤ a) → supₛ s ≤ a

ink

theorem isLUB_supₛ {α : Type u_1} [inst : CompleteSemilatticeSup α] (s : Set α) : IsLUB s (supₛ s)

ink

theorem IsLUB.supₛ_eq {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} (h : IsLUB s a) : supₛ s = a

ink

theorem le_supₛ_of_le {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} {b : α} (hb : b ∈ s) (h : a ≤ b) : a ≤ supₛ s

ink

theorem supₛ_le_supₛ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {t : Set α} (h : s ⊆ t) : supₛ s ≤ supₛ t

ink

@[simp]

theorem supₛ_le_iff {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} : supₛ s ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a

ink

theorem le_supₛ_iff {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} : a ≤ supₛ s ↔ ∀ (b : α), b ∈ upperBounds s → a ≤ b

ink

theorem le_supᵢ_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteSemilatticeSup α] {a : α} {s : ι → α} : a ≤ supᵢ s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

ink

theorem supₛ_le_supₛ_of_forall_exists_le {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {t : Set α} (h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ x ≤ y) : supₛ s ≤ supₛ t

ink

theorem supₛ_singleton {α : Type u_1} [inst : CompleteSemilatticeSup α] {a : α} : supₛ {a} = a

ink

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

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

  infₛ_le : ∀ (s : Set α) (a : α), a ∈ s → infₛ s ≤ a

• Any lower bound is less than the set infimum.

  le_infₛ : ∀ (s : Set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ infₛ s

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.

ink

theorem infₛ_le {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} : a ∈ s → infₛ s ≤ a

ink

theorem le_infₛ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} : (∀ (b : α), b ∈ s → a ≤ b) → a ≤ infₛ s

ink

theorem isGLB_infₛ {α : Type u_1} [inst : CompleteSemilatticeInf α] (s : Set α) : IsGLB s (infₛ s)

ink

theorem IsGLB.infₛ_eq {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} (h : IsGLB s a) : infₛ s = a

ink

theorem infₛ_le_of_le {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} {b : α} (hb : b ∈ s) (h : b ≤ a) : infₛ s ≤ a

ink

theorem infₛ_le_infₛ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {t : Set α} (h : s ⊆ t) : infₛ t ≤ infₛ s

ink

@[simp]

theorem le_infₛ_iff {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} : a ≤ infₛ s ↔ ∀ (b : α), b ∈ s → a ≤ b

ink

theorem infₛ_le_iff {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} : infₛ s ≤ a ↔ ∀ (b : α), b ∈ lowerBounds s → b ≤ a

ink

theorem infᵢ_le_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteSemilatticeInf α] {a : α} {s : ι → α} : infᵢ s ≤ a ↔ ∀ (b : α), (∀ (i : ι), b ≤ s i) → b ≤ a

ink

theorem infₛ_le_infₛ_of_forall_exists_le {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {t : Set α} (h : ∀ (x : α), x ∈ s → ∃ y, y ∈ t ∧ y ≤ x) : infₛ t ≤ infₛ s

ink

theorem infₛ_singleton {α : Type u_1} [inst : CompleteSemilatticeInf α] {a : α} : infₛ {a} = a

ink

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

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

  infₛ_le : ∀ (s : Set α) (a : α), a ∈ s → infₛ s ≤ a

• Any lower bound is less than the set infimum.

  le_infₛ : ∀ (s : Set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ infₛ s
• toTop : Top α
• toBot : Bot α

• Any element is less than the top one.

  le_top : ∀ (x : α), x ≤ ⊤

• Any element is more than the bottom one.

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

A complete lattice is a bounded lattice which has supᵢema and infima for every subset.

ink

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

Equations

• CompleteLattice.toBoundedOrder = BoundedOrder.mk

ink

def completeLatticeOfInf (α : Type u_1) [H1 : PartialOrder α] [H2 : InfSet α] (isGLB_infₛ : ∀ (s : Set α), IsGLB s (infₛ 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, supₛ, bot, top
  ..completeLatticeOfInf my_T _ }

Equations

• One or more equations did not get rendered due to their size.

ink

def completeLatticeOfCompleteSemilatticeInf (α : Type u_1) [inst : CompleteSemilatticeInf α] : CompleteLattice α

Any CompleteSemilatticeInf is in fact a CompleteLattice.

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

Equations

• completeLatticeOfCompleteSemilatticeInf α = completeLatticeOfInf α (_ : ∀ (s : Set α), IsGLB s (infₛ s))

ink

def completeLatticeOfSup (α : Type u_1) [H1 : PartialOrder α] [H2 : SupSet α] (isLUB_supₛ : ∀ (s : Set α), IsLUB s (supₛ 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, infₛ, bot, top
  ..completeLatticeOfSup my_T _ }

Equations

• One or more equations did not get rendered due to their size.

ink

def completeLatticeOfCompleteSemilatticeSup (α : Type u_1) [inst : CompleteSemilatticeSup α] : CompleteLattice α

Any CompleteSemilatticeSup is in fact a CompleteLattice.

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

Equations

• completeLatticeOfCompleteSemilatticeSup α = completeLatticeOfSup α (_ : ∀ (s : Set α), IsLUB s (supₛ s))

ink

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

• A linear order is total.

  le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

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

  decidable_le : DecidableRel fun x x_1 => x ≤ x_1

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

  decidable_eq : DecidableEq α

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

  decidable_lt : DecidableRel fun x x_1 => x < x_1

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

ink

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

Equations

• CompleteLinearOrder.toLinearOrder = LinearOrder.mk (_ : ∀ (a b : α), a ≤ b ∨ b ≤ a) CompleteLinearOrder.decidable_le CompleteLinearOrder.decidable_eq CompleteLinearOrder.decidable_lt

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem toDual_supₛ {α : Type u_1} [inst : CompleteLattice α] (s : Set α) : ↑OrderDual.toDual (supₛ s) = infₛ (↑OrderDual.ofDual ⁻¹' s)

ink

@[simp]

theorem toDual_infₛ {α : Type u_1} [inst : CompleteLattice α] (s : Set α) : ↑OrderDual.toDual (infₛ s) = supₛ (↑OrderDual.ofDual ⁻¹' s)

ink

@[simp]

theorem ofDual_supₛ {α : Type u_1} [inst : CompleteLattice α] (s : Set αᵒᵈ) : ↑OrderDual.ofDual (supₛ s) = infₛ (↑OrderDual.toDual ⁻¹' s)

ink

@[simp]

theorem ofDual_infₛ {α : Type u_1} [inst : CompleteLattice α] (s : Set αᵒᵈ) : ↑OrderDual.ofDual (infₛ s) = supₛ (↑OrderDual.toDual ⁻¹' s)

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

theorem infₛ_le_supₛ {α : Type u_1} [inst : CompleteLattice α] {s : Set α} (hs : Set.Nonempty s) : infₛ s ≤ supₛ s

ink

theorem supₛ_union {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} : supₛ (s ∪ t) = supₛ s ⊔ supₛ t

ink

theorem infₛ_union {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} : infₛ (s ∪ t) = infₛ s ⊓ infₛ t

ink

theorem supₛ_inter_le {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} : supₛ (s ∩ t) ≤ supₛ s ⊓ supₛ t

ink

theorem le_infₛ_inter {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} : infₛ s ⊔ infₛ t ≤ infₛ (s ∩ t)

ink

@[simp]

theorem supₛ_empty {α : Type u_1} [inst : CompleteLattice α] : supₛ ∅ = ⊥

ink

@[simp]

theorem infₛ_empty {α : Type u_1} [inst : CompleteLattice α] : infₛ ∅ = ⊤

ink

@[simp]

theorem supₛ_univ {α : Type u_1} [inst : CompleteLattice α] : supₛ Set.univ = ⊤

ink

@[simp]

theorem infₛ_univ {α : Type u_1} [inst : CompleteLattice α] : infₛ Set.univ = ⊥

ink

@[simp]

theorem supₛ_insert {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} : supₛ (insert a s) = a ⊔ supₛ s

ink

@[simp]

theorem infₛ_insert {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} : infₛ (insert a s) = a ⊓ infₛ s

ink

theorem supₛ_le_supₛ_of_subset_insert_bot {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} (h : s ⊆ insert ⊥ t) : supₛ s ≤ supₛ t

ink

theorem infₛ_le_infₛ_of_subset_insert_top {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} (h : s ⊆ insert ⊤ t) : infₛ t ≤ infₛ s

ink

@[simp]

theorem supₛ_diff_singleton_bot {α : Type u_1} [inst : CompleteLattice α] (s : Set α) : supₛ (s \ {⊥}) = supₛ s

ink

@[simp]

theorem infₛ_diff_singleton_top {α : Type u_1} [inst : CompleteLattice α] (s : Set α) : infₛ (s \ {⊤}) = infₛ s

ink

theorem supₛ_pair {α : Type u_1} [inst : CompleteLattice α] {a : α} {b : α} : supₛ {a, b} = a ⊔ b

ink

theorem infₛ_pair {α : Type u_1} [inst : CompleteLattice α] {a : α} {b : α} : infₛ {a, b} = a ⊓ b

ink

@[simp]

theorem supₛ_eq_bot {α : Type u_1} [inst : CompleteLattice α] {s : Set α} : supₛ s = ⊥ ↔ ∀ (a : α), a ∈ s → a = ⊥

ink

@[simp]

theorem infₛ_eq_top {α : Type u_1} [inst : CompleteLattice α] {s : Set α} : infₛ s = ⊤ ↔ ∀ (a : α), a ∈ s → a = ⊤

ink

theorem eq_singleton_bot_of_supₛ_eq_bot_of_nonempty {α : Type u_1} [inst : CompleteLattice α] {s : Set α} (h_sup : supₛ s = ⊥) (hne : Set.Nonempty s) : s = {⊥}

ink

theorem eq_singleton_top_of_infₛ_eq_top_of_nonempty {α : Type u_1} [inst : CompleteLattice α] {s : Set α} : infₛ s = ⊤ → Set.Nonempty s → s = {⊤}

ink

theorem supₛ_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {b : α} (h₁ : ∀ (a : α), a ∈ s → a ≤ b) (h₂ : ∀ (w : α), w < b → ∃ a, a ∈ s ∧ w < a) : supₛ s = b

Introduction rule to prove that b is the supremum of s: it suffices to check that b is larger than all elements of s, and that this is not the case of any w < b. See csupₛ_eq_of_forall_le_of_forall_lt_exists_gt for a version in conditionally complete lattices.

ink

theorem infₛ_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {b : α} : (∀ (a : α), a ∈ s → b ≤ a) → (∀ (w : α), b < w → ∃ a, a ∈ s ∧ a < w) → infₛ s = b

Introduction rule to prove that b is the infimum of s: it suffices to check that b is smaller than all elements of s, and that this is not the case of any w > b. See cinfₛ_eq_of_forall_ge_of_forall_gt_exists_lt for a version in conditionally complete lattices.

ink

theorem lt_supₛ_iff {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} {b : α} : b < supₛ s ↔ ∃ a, a ∈ s ∧ b < a

ink

theorem infₛ_lt_iff {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} {b : α} : infₛ s < b ↔ ∃ a, a ∈ s ∧ a < b

ink

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

ink

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

ink

theorem lt_supᵢ_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLinearOrder α] {a : α} {f : ι → α} : a < supᵢ f ↔ ∃ i, a < f i

ink

theorem infᵢ_lt_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLinearOrder α] {a : α} {f : ι → α} : infᵢ f < a ↔ ∃ i, f i < a

ink

theorem supₛ_range {α : Type u_1} {ι : Sort u_2} [inst : SupSet α] {f : ι → α} : supₛ (Set.range f) = supᵢ f

ink

theorem supₛ_eq_supᵢ' {α : Type u_1} [inst : SupSet α] (s : Set α) : supₛ s = ⨆ a, ↑a

ink

theorem supᵢ_congr {α : Type u_1} {ι : Sort u_2} [inst : SupSet α] {f : ι → α} {g : ι → α} (h : ∀ (i : ι), f i = g i) : (⨆ i, f i) = ⨆ i, g i

ink

theorem Function.Surjective.supᵢ_comp {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : SupSet α] {f : ι → ι'} (hf : Function.Surjective f) (g : ι' → α) : (⨆ x, g (f x)) = ⨆ y, g y

ink

theorem Equiv.supᵢ_comp {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : SupSet α] {g : ι' → α} (e : ι ≃ ι') : (⨆ x, g (↑e x)) = ⨆ y, g y

ink

theorem Function.Surjective.supᵢ_congr {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : SupSet α] {f : ι → α} {g : ι' → α} (h : ι → ι') (h1 : Function.Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) : (⨆ x, f x) = ⨆ y, g y

ink

theorem Equiv.supᵢ_congr {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : SupSet α] {f : ι → α} {g : ι' → α} (e : ι ≃ ι') (h : ∀ (x : ι), g (↑e x) = f x) : (⨆ x, f x) = ⨆ y, g y

ink

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

ink

theorem supᵢ_plift_up {α : Type u_2} {ι : Sort u_1} [inst : SupSet α] (f : PLift ι → α) : (⨆ i, f { down := i }) = ⨆ i, f i

ink

theorem supᵢ_plift_down {α : Type u_1} {ι : Sort u_2} [inst : SupSet α] (f : ι → α) : (⨆ i, f i.down) = ⨆ i, f i

ink

theorem supᵢ_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SupSet α] (g : β → α) (f : ι → β) : (⨆ b, g ↑b) = ⨆ i, g (f i)

ink

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

ink

theorem infₛ_range {α : Type u_1} {ι : Sort u_2} [inst : InfSet α] {f : ι → α} : infₛ (Set.range f) = infᵢ f

ink

theorem infₛ_eq_infᵢ' {α : Type u_1} [inst : InfSet α] (s : Set α) : infₛ s = ⨅ a, ↑a

ink

theorem infᵢ_congr {α : Type u_1} {ι : Sort u_2} [inst : InfSet α] {f : ι → α} {g : ι → α} (h : ∀ (i : ι), f i = g i) : (⨅ i, f i) = ⨅ i, g i

ink

theorem Function.Surjective.infᵢ_comp {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : InfSet α] {f : ι → ι'} (hf : Function.Surjective f) (g : ι' → α) : (⨅ x, g (f x)) = ⨅ y, g y

ink

theorem Equiv.infᵢ_comp {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : InfSet α] {g : ι' → α} (e : ι ≃ ι') : (⨅ x, g (↑e x)) = ⨅ y, g y

ink

theorem Function.Surjective.infᵢ_congr {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : InfSet α] {f : ι → α} {g : ι' → α} (h : ι → ι') (h1 : Function.Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) : (⨅ x, f x) = ⨅ y, g y

ink

theorem Equiv.infᵢ_congr {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : InfSet α] {f : ι → α} {g : ι' → α} (e : ι ≃ ι') (h : ∀ (x : ι), g (↑e x) = f x) : (⨅ x, f x) = ⨅ y, g y

ink

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

ink

theorem infᵢ_plift_up {α : Type u_2} {ι : Sort u_1} [inst : InfSet α] (f : PLift ι → α) : (⨅ i, f { down := i }) = ⨅ i, f i

ink

theorem infᵢ_plift_down {α : Type u_1} {ι : Sort u_2} [inst : InfSet α] (f : ι → α) : (⨅ i, f i.down) = ⨅ i, f i

ink

theorem infᵢ_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : InfSet α] (g : β → α) (f : ι → β) : (⨅ b, g ↑b) = ⨅ i, g (f i)

ink

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

ink

theorem le_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ι → α) (i : ι) : f i ≤ supᵢ f

ink

theorem infᵢ_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ι → α) (i : ι) : infᵢ f ≤ f i

ink

theorem le_supᵢ' {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ι → α) (i : ι) : f i ≤ supᵢ f

ink

theorem infᵢ_le' {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ι → α) (i : ι) : infᵢ f ≤ f i

ink

theorem isLUB_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} : IsLUB (Set.range f) (⨆ j, f j)

ink

theorem isGLB_infᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} : IsGLB (Set.range f) (⨅ j, f j)

ink

theorem IsLUB.supᵢ_eq {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {a : α} (h : IsLUB (Set.range f) a) : (⨆ j, f j) = a

ink

theorem IsGLB.infᵢ_eq {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {a : α} (h : IsGLB (Set.range f) a) : (⨅ j, f j) = a

ink

theorem le_supᵢ_of_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {a : α} (i : ι) (h : a ≤ f i) : a ≤ supᵢ f

ink

theorem infᵢ_le_of_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {a : α} (i : ι) (h : f i ≤ a) : infᵢ f ≤ a

ink

theorem le_supᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} (i : ι) (j : κ i) : f i j ≤ ⨆ i, ⨆ j, f i j

ink

theorem infᵢ₂_le {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} (i : ι) (j : κ i) : (⨅ i, ⨅ j, f i j) ≤ f i j

ink

theorem le_supᵢ₂_of_le {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (i : ι) (j : κ i) (h : a ≤ f i j) : a ≤ ⨆ i, ⨆ j, f i j

ink

theorem infᵢ₂_le_of_le {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (i : ι) (j : κ i) (h : f i j ≤ a) : (⨅ i, ⨅ j, f i j) ≤ a

ink

theorem supᵢ_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {a : α} (h : ∀ (i : ι), f i ≤ a) : supᵢ f ≤ a

ink

theorem le_infᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {a : α} (h : ∀ (i : ι), a ≤ f i) : a ≤ infᵢ f

ink

theorem supᵢ₂_le {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), f i j ≤ a) : (⨆ i, ⨆ j, f i j) ≤ a

ink

theorem le_infᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), a ≤ f i j) : a ≤ ⨅ i, ⨅ j, f i j

ink

theorem supᵢ₂_le_supᵢ {α : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] (κ : ι → Sort u_1) (f : ι → α) : (⨆ i, ⨆ _j, f i) ≤ ⨆ i, f i

ink

theorem infᵢ_le_infᵢ₂ {α : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] (κ : ι → Sort u_1) (f : ι → α) : (⨅ i, f i) ≤ ⨅ i, ⨅ _j, f i

ink

theorem supᵢ_mono {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {g : ι → α} (h : ∀ (i : ι), f i ≤ g i) : supᵢ f ≤ supᵢ g

ink

theorem infᵢ_mono {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {g : ι → α} (h : ∀ (i : ι), f i ≤ g i) : infᵢ f ≤ infᵢ g

ink

theorem supᵢ₂_mono {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} {g : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), f i j ≤ g i j) : (⨆ i, ⨆ j, f i j) ≤ ⨆ i, ⨆ j, g i j

ink

theorem infᵢ₂_mono {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} {g : (i : ι) → κ i → α} (h : ∀ (i : ι) (j : κ i), f i j ≤ g i j) : (⨅ i, ⨅ j, f i j) ≤ ⨅ i, ⨅ j, g i j

ink

theorem supᵢ_mono' {α : Type u_2} {ι : Sort u_3} {ι' : Sort u_1} [inst : CompleteLattice α] {f : ι → α} {g : ι' → α} (h : ∀ (i : ι), ∃ i', f i ≤ g i') : supᵢ f ≤ supᵢ g

ink

theorem infᵢ_mono' {α : Type u_2} {ι : Sort u_1} {ι' : Sort u_3} [inst : CompleteLattice α] {f : ι → α} {g : ι' → α} (h : ∀ (i' : ι'), ∃ i, f i ≤ g i') : infᵢ f ≤ infᵢ g

ink

theorem supᵢ₂_mono' {α : Type u_3} {ι : Sort u_4} {ι' : Sort u_1} {κ : ι → Sort u_5} {κ' : ι' → Sort u_2} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} {g : (i' : ι') → κ' i' → α} (h : ∀ (i : ι) (j : κ i), ∃ i' j', f i j ≤ g i' j') : (⨆ i, ⨆ j, f i j) ≤ ⨆ i, ⨆ j, g i j

ink

theorem infᵢ₂_mono' {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_4} {κ : ι → Sort u_2} {κ' : ι' → Sort u_5} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} {g : (i' : ι') → κ' i' → α} (h : ∀ (i : ι') (j : κ' i), ∃ i' j', f i' j' ≤ g i j) : (⨅ i, ⨅ j, f i j) ≤ ⨅ i, ⨅ j, g i j

ink

theorem supᵢ_const_mono {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : CompleteLattice α] {a : α} (h : ι → ι') : (⨆ _i, a) ≤ ⨆ _j, a

ink

theorem infᵢ_const_mono {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : CompleteLattice α] {a : α} (h : ι' → ι) : (⨅ _i, a) ≤ ⨅ _j, a

ink

theorem supᵢ_infᵢ_le_infᵢ_supᵢ {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : CompleteLattice α] (f : ι → ι' → α) : (⨆ i, ⨅ j, f i j) ≤ ⨅ j, ⨆ i, f i j

ink

theorem bsupᵢ_mono {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {p : ι → Prop} {q : ι → Prop} (hpq : (i : ι) → p i → q i) : (⨆ i, ⨆ _h, f i) ≤ ⨆ i, ⨆ _h, f i

ink

theorem binfᵢ_mono {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {p : ι → Prop} {q : ι → Prop} (hpq : (i : ι) → p i → q i) : (⨅ i, ⨅ _h, f i) ≤ ⨅ i, ⨅ _h, f i

ink

@[simp]

theorem supᵢ_le_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {a : α} : supᵢ f ≤ a ↔ ∀ (i : ι), f i ≤ a

ink

@[simp]

theorem le_infᵢ_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {a : α} : a ≤ infᵢ f ↔ ∀ (i : ι), a ≤ f i

ink

theorem supᵢ₂_le_iff {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} : (⨆ i, ⨆ j, f i j) ≤ a ↔ ∀ (i : ι) (j : κ i), f i j ≤ a

ink

theorem le_infᵢ₂_iff {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} : (a ≤ ⨅ i, ⨅ j, f i j) ↔ ∀ (i : ι) (j : κ i), a ≤ f i j

ink

theorem supᵢ_lt_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {a : α} : supᵢ f < a ↔ ∃ b, b < a ∧ ∀ (i : ι), f i ≤ b

ink

theorem lt_infᵢ_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {a : α} : a < infᵢ f ↔ ∃ b, a < b ∧ ∀ (i : ι), b ≤ f i

ink

theorem supₛ_eq_supᵢ {α : Type u_1} [inst : CompleteLattice α] {s : Set α} : supₛ s = ⨆ a, ⨆ h, a

ink

theorem infₛ_eq_infᵢ {α : Type u_1} [inst : CompleteLattice α] {s : Set α} : infₛ s = ⨅ a, ⨅ h, a

ink

theorem Monotone.le_map_supᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] {s : ι → α} [inst : CompleteLattice β] {f : α → β} (hf : Monotone f) : (⨆ i, f (s i)) ≤ f (supᵢ s)

ink

theorem Antitone.le_map_infᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] {s : ι → α} [inst : CompleteLattice β] {f : α → β} (hf : Antitone f) : (⨆ i, f (s i)) ≤ f (infᵢ s)

ink

theorem Monotone.le_map_supᵢ₂ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : α → β} (hf : Monotone f) (s : (i : ι) → κ i → α) : (⨆ i, ⨆ j, f (s i j)) ≤ f (⨆ i, ⨆ j, s i j)

ink

theorem Antitone.le_map_infᵢ₂ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : α → β} (hf : Antitone f) (s : (i : ι) → κ i → α) : (⨆ i, ⨆ j, f (s i j)) ≤ f (⨅ i, ⨅ j, s i j)

ink

theorem Monotone.le_map_supₛ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) : (⨆ a, ⨆ h, f a) ≤ f (supₛ s)

ink

theorem Antitone.le_map_infₛ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) : (⨆ a, ⨆ h, f a) ≤ f (infₛ s)

ink

theorem OrderIso.map_supᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] [inst : CompleteLattice β] (f : α ≃o β) (x : ι → α) : ↑(RelIso.toRelEmbedding f).toEmbedding (⨆ i, x i) = ⨆ i, ↑(RelIso.toRelEmbedding f).toEmbedding (x i)

ink

theorem OrderIso.map_infᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] [inst : CompleteLattice β] (f : α ≃o β) (x : ι → α) : ↑(RelIso.toRelEmbedding f).toEmbedding (⨅ i, x i) = ⨅ i, ↑(RelIso.toRelEmbedding f).toEmbedding (x i)

ink

theorem OrderIso.map_supₛ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] (f : α ≃o β) (s : Set α) : ↑(RelIso.toRelEmbedding f).toEmbedding (supₛ s) = ⨆ a, ⨆ h, ↑(RelIso.toRelEmbedding f).toEmbedding a

ink

theorem OrderIso.map_infₛ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] (f : α ≃o β) (s : Set α) : ↑(RelIso.toRelEmbedding f).toEmbedding (infₛ s) = ⨅ a, ⨅ h, ↑(RelIso.toRelEmbedding f).toEmbedding a

ink

theorem supᵢ_comp_le {α : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] {ι' : Sort u_1} (f : ι' → α) (g : ι → ι') : (⨆ x, f (g x)) ≤ ⨆ y, f y

ink

theorem le_infᵢ_comp {α : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] {ι' : Sort u_1} (f : ι' → α) (g : ι → ι') : (⨅ y, f y) ≤ ⨅ x, f (g x)

ink

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

ink

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

ink

theorem Antitone.map_supᵢ_le {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] {s : ι → α} [inst : CompleteLattice β] {f : α → β} (hf : Antitone f) : f (supᵢ s) ≤ ⨅ i, f (s i)

ink

theorem Monotone.map_infᵢ_le {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] {s : ι → α} [inst : CompleteLattice β] {f : α → β} (hf : Monotone f) : f (infᵢ s) ≤ ⨅ i, f (s i)

ink

theorem Antitone.map_supᵢ₂_le {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : α → β} (hf : Antitone f) (s : (i : ι) → κ i → α) : f (⨆ i, ⨆ j, s i j) ≤ ⨅ i, ⨅ j, f (s i j)

ink

theorem Monotone.map_infᵢ₂_le {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : α → β} (hf : Monotone f) (s : (i : ι) → κ i → α) : f (⨅ i, ⨅ j, s i j) ≤ ⨅ i, ⨅ j, f (s i j)

ink

theorem Antitone.map_supₛ_le {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) : f (supₛ s) ≤ ⨅ a, ⨅ h, f a

ink

theorem Monotone.map_infₛ_le {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) : f (infₛ s) ≤ ⨅ a, ⨅ h, f a

ink

theorem supᵢ_const_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {a : α} : (⨆ _i, a) ≤ a

ink

theorem le_infᵢ_const {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {a : α} : a ≤ ⨅ _i, a

ink

theorem supᵢ_const {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {a : α} [inst : Nonempty ι] : (⨆ _b, a) = a

ink

theorem infᵢ_const {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {a : α} [inst : Nonempty ι] : (⨅ _b, a) = a

ink

@[simp]

theorem supᵢ_bot {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] : (⨆ _i, ⊥) = ⊥

ink

@[simp]

theorem infᵢ_top {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] : (⨅ _i, ⊤) = ⊤

ink

@[simp]

theorem supᵢ_eq_bot {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {s : ι → α} : supᵢ s = ⊥ ↔ ∀ (i : ι), s i = ⊥

ink

@[simp]

theorem infᵢ_eq_top {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {s : ι → α} : infᵢ s = ⊤ ↔ ∀ (i : ι), s i = ⊤

ink

theorem supᵢ₂_eq_bot {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} : (⨆ i, ⨆ j, f i j) = ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥

ink

theorem infᵢ₂_eq_top {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} : (⨅ i, ⨅ j, f i j) = ⊤ ↔ ∀ (i : ι) (j : κ i), f i j = ⊤

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

theorem supᵢ_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} {ι : Sort u_2} [inst : 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 csupᵢ_eq_of_forall_le_of_forall_lt_exists_gt for a version in conditionally complete lattices.

ink

theorem infᵢ_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} {ι : Sort u_2} [inst : 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 cinfᵢ_eq_of_forall_ge_of_forall_gt_exists_lt for a version in conditionally complete lattices.

ink

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

ink

theorem supᵢ_eq_if {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst : Decidable p] (a : α) : (⨆ _h, a) = if p then a else ⊥

ink

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

ink

theorem infᵢ_eq_if {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst : Decidable p] (a : α) : (⨅ _h, a) = if p then a else ⊤

ink

theorem supᵢ_comm {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : CompleteLattice α] {f : ι → ι' → α} : (⨆ i, ⨆ j, f i j) = ⨆ j, ⨆ i, f i j

ink

theorem infᵢ_comm {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : CompleteLattice α] {f : ι → ι' → α} : (⨅ i, ⨅ j, f i j) = ⨅ j, ⨅ i, f i j

ink

theorem supᵢ₂_comm {α : Type u_5} [inst : CompleteLattice α] {ι₁ : Sort u_1} {ι₂ : Sort u_2} {κ₁ : ι₁ → Sort u_3} {κ₂ : ι₂ → Sort u_4} (f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α) : (⨆ i₁, ⨆ j₁, ⨆ i₂, ⨆ j₂, f i₁ j₁ i₂ j₂) = ⨆ i₂, ⨆ j₂, ⨆ i₁, ⨆ j₁, f i₁ j₁ i₂ j₂

ink

theorem infᵢ₂_comm {α : Type u_5} [inst : CompleteLattice α] {ι₁ : Sort u_1} {ι₂ : Sort u_2} {κ₁ : ι₁ → Sort u_3} {κ₂ : ι₂ → Sort u_4} (f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α) : (⨅ i₁, ⨅ j₁, ⨅ i₂, ⨅ j₂, f i₁ j₁ i₂ j₂) = ⨅ i₂, ⨅ j₂, ⨅ i₁, ⨅ j₁, f i₁ j₁ i₂ j₂

ink

@[simp]

theorem supᵢ_supᵢ_eq_left {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {b : β} {f : (x : β) → x = b → α} : (⨆ x, ⨆ h, f x h) = f b (_ : b = b)

ink

@[simp]

theorem infᵢ_infᵢ_eq_left {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {b : β} {f : (x : β) → x = b → α} : (⨅ x, ⨅ h, f x h) = f b (_ : b = b)

ink

@[simp]

theorem supᵢ_supᵢ_eq_right {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {b : β} {f : (x : β) → b = x → α} : (⨆ x, ⨆ h, f x h) = f b (_ : b = b)

ink

@[simp]

theorem infᵢ_infᵢ_eq_right {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {b : β} {f : (x : β) → b = x → α} : (⨅ x, ⨅ h, f x h) = f b (_ : b = b)

ink

theorem supᵢ_subtype {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ι → Prop} {f : Subtype p → α} : supᵢ f = ⨆ i, ⨆ h, f { val := i, property := h }

ink

theorem infᵢ_subtype {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ι → Prop} {f : Subtype p → α} : infᵢ f = ⨅ i, ⨅ h, f { val := i, property := h }

ink

theorem supᵢ_subtype' {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} : (⨆ i, ⨆ h, f i h) = ⨆ x, f (↑x) x.property

ink

theorem infᵢ_subtype' {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} : (⨅ i, ⨅ h, f i h) = ⨅ x, f (↑x) x.property

ink

theorem supᵢ_subtype'' {α : Type u_2} [inst : CompleteLattice α] {ι : Type u_1} (s : Set ι) (f : ι → α) : (⨆ i, f ↑i) = ⨆ t, ⨆ _H, f t

ink

theorem infᵢ_subtype'' {α : Type u_2} [inst : CompleteLattice α] {ι : Type u_1} (s : Set ι) (f : ι → α) : (⨅ i, f ↑i) = ⨅ t, ⨅ _H, f t

ink

theorem bsupᵢ_const {α : Type u_2} [inst : CompleteLattice α] {ι : Type u_1} {a : α} {s : Set ι} (hs : Set.Nonempty s) : (⨆ i, ⨆ h, a) = a

ink

theorem binfᵢ_const {α : Type u_2} [inst : CompleteLattice α] {ι : Type u_1} {a : α} {s : Set ι} (hs : Set.Nonempty s) : (⨅ i, ⨅ h, a) = a

ink

theorem supᵢ_sup_eq {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {g : ι → α} : (⨆ x, f x ⊔ g x) = (⨆ x, f x) ⊔ ⨆ x, g x

ink

theorem infᵢ_inf_eq {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ι → α} {g : ι → α} : (⨅ x, f x ⊓ g x) = (⨅ x, f x) ⊓ ⨅ x, g x

ink

theorem supᵢ_sup {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : Nonempty ι] {f : ι → α} {a : α} : (⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a

ink

theorem infᵢ_inf {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : Nonempty ι] {f : ι → α} {a : α} : (⨅ x, f x) ⊓ a = ⨅ x, f x ⊓ a

ink

theorem sup_supᵢ {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : Nonempty ι] {f : ι → α} {a : α} : (a ⊔ ⨆ x, f x) = ⨆ x, a ⊔ f x

ink

theorem inf_infᵢ {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : Nonempty ι] {f : ι → α} {a : α} : (a ⊓ ⨅ x, f x) = ⨅ x, a ⊓ f x

ink

theorem bsupᵢ_sup {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} (h : ∃ i, p i) : (⨆ i, ⨆ h, f i h) ⊔ a = ⨆ i, ⨆ h, f i h ⊔ a

ink

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

ink

theorem binfᵢ_inf {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α} (h : ∃ i, p i) : (⨅ i, ⨅ h, f i h) ⊓ a = ⨅ i, ⨅ h, f i h ⊓ a

ink

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

supᵢ and infᵢ under Prop

ink

theorem supᵢ_false {α : Type u_1} [inst : CompleteLattice α] {s : False → α} : supᵢ s = ⊥

ink

theorem infᵢ_false {α : Type u_1} [inst : CompleteLattice α] {s : False → α} : infᵢ s = ⊤

ink

theorem supᵢ_true {α : Type u_1} [inst : CompleteLattice α] {s : True → α} : supᵢ s = s trivial

ink

theorem infᵢ_true {α : Type u_1} [inst : CompleteLattice α] {s : True → α} : infᵢ s = s trivial

ink

@[simp]

theorem supᵢ_exists {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ι → Prop} {f : Exists p → α} : (⨆ x, f x) = ⨆ i, ⨆ h, f (_ : Exists p)

ink

@[simp]

theorem infᵢ_exists {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ι → Prop} {f : Exists p → α} : (⨅ x, f x) = ⨅ i, ⨅ h, f (_ : Exists p)

ink

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

ink

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

ink

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

The symmetric case of supᵢ_and, useful for rewriting into a supremum over a conjunction

ink

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

The symmetric case of infᵢ_and, useful for rewriting into a infimum over a conjunction

ink

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

ink

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

ink

theorem supᵢ_dite {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (p : ι → Prop) [inst : 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, f i h) ⊔ ⨆ i, ⨆ h, g i h

ink

theorem infᵢ_dite {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (p : ι → Prop) [inst : 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, f i h) ⊓ ⨅ i, ⨅ h, g i h

ink

theorem supᵢ_ite {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (p : ι → Prop) [inst : DecidablePred p] (f : ι → α) (g : ι → α) : (⨆ i, if p i then f i else g i) = (⨆ i, ⨆ _h, f i) ⊔ ⨆ i, ⨆ _h, g i

ink

theorem infᵢ_ite {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (p : ι → Prop) [inst : DecidablePred p] (f : ι → α) (g : ι → α) : (⨅ i, if p i then f i else g i) = (⨅ i, ⨅ _h, f i) ⊓ ⨅ i, ⨅ _h, g i

ink

theorem supᵢ_range {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] {g : β → α} {f : ι → β} : (⨆ b, ⨆ h, g b) = ⨆ i, g (f i)

ink

theorem infᵢ_range {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] {g : β → α} {f : ι → β} : (⨅ b, ⨅ h, g b) = ⨅ i, g (f i)

ink

theorem supₛ_image {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {s : Set β} {f : β → α} : supₛ (f '' s) = ⨆ a, ⨆ h, f a

ink

theorem infₛ_image {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {s : Set β} {f : β → α} : infₛ (f '' s) = ⨅ a, ⨅ h, f a

ink

theorem supᵢ_emptyset {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} : (⨆ x, ⨆ h, f x) = ⊥

ink

theorem infᵢ_emptyset {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} : (⨅ x, ⨅ h, f x) = ⊤

ink

theorem supᵢ_univ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} : (⨆ x, ⨆ h, f x) = ⨆ x, f x

ink

theorem infᵢ_univ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} : (⨅ x, ⨅ h, f x) = ⨅ x, f x

ink

theorem supᵢ_union {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : β → α} {s : Set β} {t : Set β} : (⨆ x, ⨆ h, f x) = (⨆ x, ⨆ h, f x) ⊔ ⨆ x, ⨆ h, f x

ink

theorem infᵢ_union {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : β → α} {s : Set β} {t : Set β} : (⨅ x, ⨅ h, f x) = (⨅ x, ⨅ h, f x) ⊓ ⨅ x, ⨅ h, f x

ink

theorem supᵢ_split {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (p : β → Prop) : (⨆ i, f i) = (⨆ i, ⨆ _h, f i) ⊔ ⨆ i, ⨆ _h, f i

ink

theorem infᵢ_split {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (p : β → Prop) : (⨅ i, f i) = (⨅ i, ⨅ _h, f i) ⊓ ⨅ i, ⨅ _h, f i

ink

theorem supᵢ_split_single {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (i₀ : β) : (⨆ i, f i) = f i₀ ⊔ ⨆ i, ⨆ _h, f i

ink

theorem infᵢ_split_single {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (i₀ : β) : (⨅ i, f i) = f i₀ ⊓ ⨅ i, ⨅ _h, f i

ink

theorem supᵢ_le_supᵢ_of_subset {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : β → α} {s : Set β} {t : Set β} : s ⊆ t → (⨆ x, ⨆ h, f x) ≤ ⨆ x, ⨆ h, f x

ink

theorem infᵢ_le_infᵢ_of_subset {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : β → α} {s : Set β} {t : Set β} : s ⊆ t → (⨅ x, ⨅ h, f x) ≤ ⨅ x, ⨅ h, f x

ink

theorem supᵢ_insert {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : β → α} {s : Set β} {b : β} : (⨆ x, ⨆ h, f x) = f b ⊔ ⨆ x, ⨆ h, f x

ink

theorem infᵢ_insert {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : β → α} {s : Set β} {b : β} : (⨅ x, ⨅ h, f x) = f b ⊓ ⨅ x, ⨅ h, f x

ink

theorem supᵢ_singleton {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {b : β} : (⨆ x, ⨆ h, f x) = f b

ink

theorem infᵢ_singleton {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {b : β} : (⨅ x, ⨅ h, f x) = f b

ink

theorem supᵢ_pair {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {a : β} {b : β} : (⨆ x, ⨆ h, f x) = f a ⊔ f b

ink

theorem infᵢ_pair {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {a : β} {b : β} : (⨅ x, ⨅ h, f x) = f a ⊓ f b

ink

theorem supᵢ_image {α : Type u_3} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_1} {f : β → γ} {g : γ → α} {t : Set β} : (⨆ c, ⨆ h, g c) = ⨆ b, ⨆ h, g (f b)

ink

theorem infᵢ_image {α : Type u_3} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_1} {f : β → γ} {g : γ → α} {t : Set β} : (⨅ c, ⨅ h, g c) = ⨅ b, ⨅ h, g (f b)

ink

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

ink

theorem infᵢ_extend_top {α : Type u_3} {β : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {e : ι → β} (he : Function.Injective e) (f : ι → α) : (⨅ j, Function.extend e f ⊤ j) = infᵢ f

supᵢ and infᵢ under Type

ink

theorem supᵢ_of_empty' {α : Type u_1} {ι : Sort u_2} [inst : SupSet α] [inst : IsEmpty ι] (f : ι → α) : supᵢ f = supₛ ∅

ink

theorem infᵢ_of_empty' {α : Type u_1} {ι : Sort u_2} [inst : InfSet α] [inst : IsEmpty ι] (f : ι → α) : infᵢ f = infₛ ∅

ink

theorem supᵢ_of_empty {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : IsEmpty ι] (f : ι → α) : supᵢ f = ⊥

ink

theorem infᵢ_of_empty {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : IsEmpty ι] (f : ι → α) : infᵢ f = ⊤

ink

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

ink

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

ink

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

ink

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

ink

theorem isGLB_binfᵢ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {s : Set β} {f : β → α} : IsGLB (f '' s) (⨅ x, ⨅ h, f x)

ink

theorem isLUB_bsupᵢ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {s : Set β} {f : β → α} : IsLUB (f '' s) (⨆ x, ⨆ h, f x)

ink

theorem supᵢ_sigma {α : Type u_3} {β : Type u_2} [inst : CompleteLattice α] {p : β → Type u_1} {f : Sigma p → α} : (⨆ x, f x) = ⨆ i, ⨆ j, f { fst := i, snd := j }

ink

theorem infᵢ_sigma {α : Type u_3} {β : Type u_2} [inst : CompleteLattice α] {p : β → Type u_1} {f : Sigma p → α} : (⨅ x, f x) = ⨅ i, ⨅ j, f { fst := i, snd := j }

ink

theorem supᵢ_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β × γ → α} : (⨆ x, f x) = ⨆ i, ⨆ j, f (i, j)

ink

theorem infᵢ_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β × γ → α} : (⨅ x, f x) = ⨅ i, ⨅ j, f (i, j)

ink

theorem bsupᵢ_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ} : (⨆ x, ⨆ h, f x) = ⨆ a, ⨆ h, ⨆ b, ⨆ h, f (a, b)

ink

theorem binfᵢ_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ} : (⨅ x, ⨅ h, f x) = ⨅ a, ⨅ h, ⨅ b, ⨅ h, f (a, b)

ink

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

ink

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

ink

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

ink

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

ink

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

A version of supᵢ_option useful for rewriting right-to-left.

ink

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

A version of infᵢ_option useful for rewriting right-to-left.

ink

theorem supᵢ_ne_bot_subtype {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (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.

ink

theorem infᵢ_ne_top_subtype {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (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.

ink

theorem supₛ_image2 {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} : supₛ (Set.image2 f s t) = ⨆ a, ⨆ h, ⨆ b, ⨆ h, f a b

ink

theorem infₛ_image2 {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} : infₛ (Set.image2 f s t) = ⨅ a, ⨅ h, ⨅ b, ⨅ h, f a b

supᵢ and infᵢ under ℕ

ink

theorem supᵢ_ge_eq_supᵢ_nat_add {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ) : (⨆ i, ⨆ h, u i) = ⨆ i, u (i + n)

ink

theorem infᵢ_ge_eq_infᵢ_nat_add {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ) : (⨅ i, ⨅ h, u i) = ⨅ i, u (i + n)

ink

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

ink

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

ink

theorem supᵢ_infᵢ_ge_nat_add {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → α) (k : ℕ) : (⨆ n, ⨅ i, ⨅ h, f (i + k)) = ⨆ n, ⨅ i, ⨅ h, f i

ink

theorem infᵢ_supᵢ_ge_nat_add {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → α) (k : ℕ) : (⨅ n, ⨆ i, ⨆ h, f (i + k)) = ⨅ n, ⨆ i, ⨆ h, f i

ink

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

ink

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

ink

theorem infᵢ_nat_gt_zero_eq {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → α) : (⨅ i, ⨅ h, f i) = ⨅ i, f (i + 1)

ink

theorem supᵢ_nat_gt_zero_eq {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → α) : (⨆ i, ⨆ h, f i) = ⨆ i, f (i + 1)

ink

theorem supᵢ_eq_top {α : Type u_1} {ι : Sort u_2} [inst : CompleteLinearOrder α] (f : ι → α) : supᵢ f = ⊤ ↔ ∀ (b : α), b < ⊤ → ∃ i, b < f i

ink

theorem infᵢ_eq_bot {α : Type u_1} {ι : Sort u_2} [inst : CompleteLinearOrder α] (f : ι → α) : infᵢ f = ⊥ ↔ ∀ (b : α), b > ⊥ → ∃ i, f i < b

Instances

ink

instance Prop.completeLattice : CompleteLattice Prop

Equations

• One or more equations did not get rendered due to their size.

ink

noncomputable instance Prop.completeLinearOrder : CompleteLinearOrder Prop

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem supₛ_Prop_eq {s : Set Prop} : supₛ s = ∃ p, p ∈ s ∧ p

ink

@[simp]

theorem infₛ_Prop_eq {s : Set Prop} : infₛ s = ∀ (p : Prop), p ∈ s → p

ink

@[simp]

theorem supᵢ_Prop_eq {ι : Sort u_1} {p : ι → Prop} : (⨆ i, p i) = ∃ i, p i

ink

@[simp]

theorem infᵢ_Prop_eq {ι : Sort u_1} {p : ι → Prop} : (⨅ i, p i) = ((i : ι) → p i)

ink

instance Pi.supSet {α : Type u_1} {β : α → Type u_2} [inst : (i : α) → SupSet (β i)] : SupSet ((i : α) → β i)

Equations

• Pi.supSet = { supₛ := fun s i => ⨆ f, ↑f i }

ink

instance Pi.infSet {α : Type u_1} {β : α → Type u_2} [inst : (i : α) → InfSet (β i)] : InfSet ((i : α) → β i)

Equations

• Pi.infSet = { infₛ := fun s i => ⨅ f, ↑f i }

ink

instance Pi.completeLattice {α : Type u_1} {β : α → Type u_2} [inst : (i : α) → CompleteLattice (β i)] : CompleteLattice ((i : α) → β i)

Equations

• One or more equations did not get rendered due to their size.

ink

theorem supₛ_apply {α : Type u_1} {β : α → Type u_2} [inst : (i : α) → SupSet (β i)] {s : Set ((a : α) → β a)} {a : α} : supₛ ((a : α) → β a) Pi.supSet s a = ⨆ f, ↑f a

ink

theorem infₛ_apply {α : Type u_1} {β : α → Type u_2} [inst : (i : α) → InfSet (β i)] {s : Set ((a : α) → β a)} {a : α} : infₛ ((a : α) → β a) Pi.infSet s a = ⨅ f, ↑f a

ink

@[simp]

theorem supᵢ_apply {α : Type u_1} {β : α → Type u_2} {ι : Sort u_3} [inst : (i : α) → SupSet (β i)] {f : ι → (a : α) → β a} {a : α} : supᵢ ((a : α) → β a) Pi.supSet ι (fun i => f i) a = ⨆ i, f i a

ink

@[simp]

theorem infᵢ_apply {α : Type u_1} {β : α → Type u_2} {ι : Sort u_3} [inst : (i : α) → InfSet (β i)] {f : ι → (a : α) → β a} {a : α} : infᵢ ((a : α) → β a) Pi.infSet ι (fun i => f i) a = ⨅ i, f i a

ink

theorem unary_relation_supₛ_iff {α : Type u_1} (s : Set (α → Prop)) {a : α} : supₛ s a ↔ ∃ r, r ∈ s ∧ r a

ink

theorem unary_relation_infₛ_iff {α : Type u_1} (s : Set (α → Prop)) {a : α} : infₛ s a ↔ (r : α → Prop) → r ∈ s → r a

ink

theorem binary_relation_supₛ_iff {α : Type u_1} {β : Type u_2} (s : Set (α → β → Prop)) {a : α} {b : β} : supₛ s a b ↔ ∃ r, r ∈ s ∧ r a b

ink

theorem binary_relation_infₛ_iff {α : Type u_1} {β : Type u_2} (s : Set (α → β → Prop)) {a : α} {b : β} : infₛ s a b ↔ (r : α → β → Prop) → r ∈ s → r a b

ink

theorem monotone_supₛ_of_monotone {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : CompleteLattice β] {s : Set (α → β)} (m_s : ∀ (f : α → β), f ∈ s → Monotone f) : Monotone (supₛ s)

ink

theorem monotone_infₛ_of_monotone {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : CompleteLattice β] {s : Set (α → β)} (m_s : ∀ (f : α → β), f ∈ s → Monotone f) : Monotone (infₛ s)

ink

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

Equations

• Prod.supSet α β = { supₛ := fun s => (supₛ (Prod.fst '' s), supₛ (Prod.snd '' s)) }

ink

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

Equations

• Prod.infSet α β = { infₛ := fun s => (infₛ (Prod.fst '' s), infₛ (Prod.snd '' s)) }

ink

theorem Prod.fst_infₛ {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst : InfSet β] (s : Set (α × β)) : (infₛ s).fst = infₛ (Prod.fst '' s)

ink

theorem Prod.snd_infₛ {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst : InfSet β] (s : Set (α × β)) : (infₛ s).snd = infₛ (Prod.snd '' s)

ink

theorem Prod.swap_infₛ {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst : InfSet β] (s : Set (α × β)) : Prod.swap (infₛ s) = infₛ (Prod.swap '' s)

ink

theorem Prod.fst_supₛ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst : SupSet β] (s : Set (α × β)) : (supₛ s).fst = supₛ (Prod.fst '' s)

ink

theorem Prod.snd_supₛ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst : SupSet β] (s : Set (α × β)) : (supₛ s).snd = supₛ (Prod.snd '' s)

ink

theorem Prod.swap_supₛ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst : SupSet β] (s : Set (α × β)) : Prod.swap (supₛ s) = supₛ (Prod.swap '' s)

ink

theorem Prod.fst_infᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : InfSet α] [inst : InfSet β] (f : ι → α × β) : (infᵢ f).fst = ⨅ i, (f i).fst

ink

theorem Prod.snd_infᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : InfSet α] [inst : InfSet β] (f : ι → α × β) : (infᵢ f).snd = ⨅ i, (f i).snd

ink

theorem Prod.swap_infᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : InfSet α] [inst : InfSet β] (f : ι → α × β) : Prod.swap (infᵢ f) = ⨅ i, Prod.swap (f i)

ink

theorem Prod.infᵢ_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : InfSet α] [inst : InfSet β] (f : ι → α) (g : ι → β) : (⨅ i, (f i, g i)) = (⨅ i, f i, ⨅ i, g i)

ink

theorem Prod.fst_supᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SupSet α] [inst : SupSet β] (f : ι → α × β) : (supᵢ f).fst = ⨆ i, (f i).fst

ink

theorem Prod.snd_supᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SupSet α] [inst : SupSet β] (f : ι → α × β) : (supᵢ f).snd = ⨆ i, (f i).snd

ink

theorem Prod.swap_supᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SupSet α] [inst : SupSet β] (f : ι → α × β) : Prod.swap (supᵢ f) = ⨆ i, Prod.swap (f i)

ink

theorem Prod.supᵢ_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SupSet α] [inst : SupSet β] (f : ι → α) (g : ι → β) : (⨆ i, (f i, g i)) = (⨆ i, f i, ⨆ i, g i)

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

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

ink

theorem sup_infₛ_le_infᵢ_sup {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} : a ⊔ infₛ s ≤ ⨅ b, ⨅ h, a ⊔ b

This is a weaker version of sup_infₛ_eq

ink

theorem supᵢ_inf_le_inf_supₛ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} : (⨆ b, ⨆ h, a ⊓ b) ≤ a ⊓ supₛ s

This is a weaker version of inf_supₛ_eq

ink

theorem infₛ_sup_le_infᵢ_sup {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} : infₛ s ⊔ a ≤ ⨅ b, ⨅ h, b ⊔ a

This is a weaker version of infₛ_sup_eq

ink

theorem supᵢ_inf_le_supₛ_inf {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} : (⨆ b, ⨆ h, b ⊓ a) ≤ supₛ s ⊓ a

This is a weaker version of supₛ_inf_eq

ink

theorem le_supᵢ_inf_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ι → α) (g : ι → α) : (⨆ i, f i ⊓ g i) ≤ (⨆ i, f i) ⊓ ⨆ i, g i

ink

theorem infᵢ_sup_infᵢ_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ι → α) (g : ι → α) : ((⨅ i, f i) ⊔ ⨅ i, g i) ≤ ⨅ i, f i ⊔ g i

ink

theorem disjoint_supₛ_left {α : Type u_1} [inst : CompleteLattice α] {a : Set α} {b : α} (d : Disjoint (supₛ a) b) {i : α} (hi : i ∈ a) : Disjoint i b

ink

theorem disjoint_supₛ_right {α : Type u_1} [inst : CompleteLattice α] {a : Set α} {b : α} (d : Disjoint b (supₛ a)) {i : α} (hi : i ∈ a) : Disjoint b i

ink

def Function.Injective.completeLattice {α : Type u_1} {β : Type u_2} [inst : Sup α] [inst : Inf α] [inst : SupSet α] [inst : InfSet α] [inst : Top α] [inst : Bot α] [inst : 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_supₛ : ∀ (s : Set α), f (supₛ s) = ⨆ a, ⨆ h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = ⨅ a, ⨅ h, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : CompleteLattice α

Pullback a CompleteLattice along an injection.

Equations

• One or more equations did not get rendered due to their size.