Mathlib.Order.CompleteLattice.Basic

iSup_ulift theorem

{ι : Type*} [SupSet α] (f : ULift ι → α) : ⨆ i : ULift ι, f i = ⨆ i, f (.up i)

Full source

@[simp] lemma iSup_ulift {ι : Type*} [SupSet α] (f : ULift ι → α) :
    ⨆ i : ULift ι, f i = ⨆ i, f (.up i) := by simp [iSup]; congr with x; simp

Supremum Preservation under ULift

Informal description

For any type $\iota$ and a complete lattice $\alpha$, given a function $f : \text{ULift}\,\iota \to \alpha$, the supremum of $f$ over $\text{ULift}\,\iota$ is equal to the supremum of $f$ over $\iota$ when lifted via $\text{ULift.up}$. In symbols: \[ \bigsqcup_{i : \text{ULift}\,\iota} f(i) = \bigsqcup_{i : \iota} f(\text{up}\,i). \]

iInf_ulift theorem

{ι : Type*} [InfSet α] (f : ULift ι → α) : ⨅ i : ULift ι, f i = ⨅ i, f (.up i)

Full source

@[simp] lemma iInf_ulift {ι : Type*} [InfSet α] (f : ULift ι → α) :
    ⨅ i : ULift ι, f i = ⨅ i, f (.up i) := by simp [iInf]; congr with x; simp

Infimum Preservation under ULift

Informal description

For any type $\iota$ and a complete lattice $\alpha$, given a function $f : \text{ULift}\,\iota \to \alpha$, the infimum of $f$ over $\text{ULift}\,\iota$ is equal to the infimum of $f$ over $\iota$ when lifted via $\text{ULift.up}$. In symbols: \[ \bigsqcap_{i : \text{ULift}\,\iota} f(i) = \bigsqcap_{i : \iota} f(\text{up}\,i). \]

sSup_le_sSup_of_forall_exists_le theorem

(h : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) : sSup s ≤ sSup t

Full source

theorem sSup_le_sSup_of_forall_exists_le (h : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) : sSup s ≤ sSup t :=
  le_sSup_iff.2 fun _ hb =>
    sSup_le fun a ha =>
      let ⟨_, hct, hac⟩ := h a ha
      hac.trans (hb hct)

Comparison of Suprema via Element-wise Inequality

Informal description

For any two subsets $s$ and $t$ in a complete lattice, if for every element $x \in s$ there exists an element $y \in t$ such that $x \leq y$, then the supremum of $s$ is less than or equal to the supremum of $t$. In symbols: \[ (\forall x \in s, \exists y \in t, x \leq y) \implies \bigvee s \leq \bigvee t. \]

sSup_singleton theorem

{a : α} : sSup { a } = a

Full source

@[simp]
theorem sSup_singleton {a : α} : sSup {a} = a :=
  isLUB_singleton.sSup_eq

Supremum of a Singleton Set is the Element Itself

Informal description

For any element $a$ in a complete lattice $\alpha$, the supremum of the singleton set $\{a\}$ is equal to $a$, i.e., $\bigvee \{a\} = a$.

sInf_le_sInf_of_forall_exists_le theorem

(h : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) : sInf t ≤ sInf s

Full source

theorem sInf_le_sInf_of_forall_exists_le (h : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) : sInf t ≤ sInf s :=
  le_sInf fun x hx ↦ let ⟨_y, hyt, hyx⟩ := h x hx; sInf_le_of_le hyt hyx

Infimum Comparison Under Elementwise Lower Bounds: $\bigwedge t \leq \bigwedge s$ when each $x \in s$ has a lower bound in $t$

Informal description

For any non-empty subsets $s$ and $t$ of a complete meet-semilattice $\alpha$, if for every $x \in s$ there exists $y \in t$ such that $y \leq x$, then the infimum of $t$ is less than or equal to the infimum of $s$, i.e., $\bigwedge t \leq \bigwedge s$.

sInf_singleton theorem

{a : α} : sInf { a } = a

Full source

@[simp]
theorem sInf_singleton {a : α} : sInf {a} = a :=
  isGLB_singleton.sInf_eq

Infimum of a Singleton Set is the Element Itself

Informal description

For any element $a$ in a complete meet-semilattice $\alpha$, the infimum of the singleton set $\{a\}$ is equal to $a$, i.e., $\bigwedge \{a\} = a$.

sInf_le_sSup theorem

(hs : s.Nonempty) : sInf s ≤ sSup s

Full source

theorem sInf_le_sSup (hs : s.Nonempty) : sInf s ≤ sSup s :=
  isGLB_le_isLUB (isGLB_sInf s) (isLUB_sSup s) hs

Infimum Does Not Exceed Supremum for Nonempty Sets

Informal description

For any nonempty subset $s$ of a complete lattice, the infimum of $s$ is less than or equal to the supremum of $s$, i.e., $\bigwedge s \leq \bigvee s$.

sSup_union theorem

{s t : Set α} : sSup (s ∪ t) = sSup s ⊔ sSup t

Full source

theorem sSup_union {s t : Set α} : sSup (s ∪ t) = sSupsSup s ⊔ sSup t :=
  ((isLUB_sSup s).union (isLUB_sSup t)).sSup_eq

Supremum of Union Equals Join of Suprema in Complete Lattices

Informal description

For any two sets $s$ and $t$ in a complete lattice $\alpha$, the supremum of their union equals the supremum of $s$ joined with the supremum of $t$, i.e., \[ \bigvee (s \cup t) = \left(\bigvee s\right) \sqcup \left(\bigvee t\right). \]

sInf_union theorem

{s t : Set α} : sInf (s ∪ t) = sInf s ⊓ sInf t

Full source

theorem sInf_union {s t : Set α} : sInf (s ∪ t) = sInfsInf s ⊓ sInf t :=
  ((isGLB_sInf s).union (isGLB_sInf t)).sInf_eq

Infimum of Union Equals Infimum of Infima in Complete Lattices

Informal description

For any two sets $s$ and $t$ in a complete lattice $\alpha$, the infimum of their union is equal to the infimum of their individual infima, i.e., \[ \bigwedge (s \cup t) = \left(\bigwedge s\right) \sqcap \left(\bigwedge t\right). \]

sSup_inter_le theorem

{s t : Set α} : sSup (s ∩ t) ≤ sSup s ⊓ sSup t

Full source

theorem sSup_inter_le {s t : Set α} : sSup (s ∩ t) ≤ sSupsSup s ⊓ sSup t :=
  sSup_le fun _ hb => le_inf (le_sSup hb.1) (le_sSup hb.2)

Supremum of Intersection is Bounded by Infimum of Suprema

Informal description

For any two sets $s$ and $t$ in a complete lattice $\alpha$, the supremum of their intersection is less than or equal to the infimum of their suprema, i.e., \[ \bigvee (s \cap t) \leq \left(\bigvee s\right) \sqcap \left(\bigvee t\right). \]

le_sInf_inter theorem

{s t : Set α} : sInf s ⊔ sInf t ≤ sInf (s ∩ t)

Full source

theorem le_sInf_inter {s t : Set α} : sInfsInf s ⊔ sInf t ≤ sInf (s ∩ t) :=
  @sSup_inter_le αᵒᵈ _ _ _

Infimum-Supremum Inequality for Set Intersection

Informal description

For any two sets $s$ and $t$ in a complete lattice $\alpha$, the supremum of their infima is less than or equal to the infimum of their intersection, i.e., \[ \left(\bigwedge s\right) \sqcup \left(\bigwedge t\right) \leq \bigwedge (s \cap t). \]

sSup_empty theorem

: sSup ∅ = (⊥ : α)

Full source

@[simp]
theorem sSup_empty : sSup ∅ = (⊥ : α) :=
  (@isLUB_empty α _ _).sSup_eq

Supremum of Empty Set is Bottom Element

Informal description

In a complete lattice $\alpha$, the supremum of the empty set is equal to the bottom element $\bot$, i.e., \[ \bigvee \emptyset = \bot. \]

sInf_empty theorem

: sInf ∅ = (⊤ : α)

Full source

@[simp]
theorem sInf_empty : sInf ∅ = (⊤ : α) :=
  (@isGLB_empty α _ _).sInf_eq

$\inf \emptyset = \top$ in a complete lattice

Informal description

In a complete lattice $\alpha$, the infimum of the empty set is equal to the top element $\top$.

sSup_univ theorem

: sSup univ = (⊤ : α)

Full source

@[simp]
theorem sSup_univ : sSup univ = (⊤ : α) :=
  (@isLUB_univ α _ _).sSup_eq

Supremum of Universal Set Equals Top Element

Informal description

In a complete lattice $\alpha$, the supremum of the universal set (the set containing all elements of $\alpha$) is equal to the top element $\top$.

sInf_univ theorem

: sInf univ = (⊥ : α)

Full source

@[simp]
theorem sInf_univ : sInf univ = (⊥ : α) :=
  (@isGLB_univ α _ _).sInf_eq

Infimum of Universal Set Equals Bottom Element

Informal description

In a complete lattice $\alpha$, the infimum of the universal set (the set containing all elements of $\alpha$) is equal to the bottom element $\bot$.

sSup_insert theorem

{a : α} {s : Set α} : sSup (insert a s) = a ⊔ sSup s

Full source

@[simp]
theorem sSup_insert {a : α} {s : Set α} : sSup (insert a s) = a ⊔ sSup s :=
  ((isLUB_sSup s).insert a).sSup_eq

Supremum of Inserted Set Equals Join of Element and Supremum

Informal description

For any element $a$ and any subset $s$ of a complete lattice $\alpha$, the supremum of the set $\{a\} \cup s$ is equal to the join of $a$ and the supremum of $s$, i.e., \[ \bigvee (\{a\} \cup s) = a \sqcup \bigvee s. \]

sInf_insert theorem

{a : α} {s : Set α} : sInf (insert a s) = a ⊓ sInf s

Full source

@[simp]
theorem sInf_insert {a : α} {s : Set α} : sInf (insert a s) = a ⊓ sInf s :=
  ((isGLB_sInf s).insert a).sInf_eq

Infimum of Inserted Set Equals Meet of Element and Infimum

Informal description

For any element $a$ and subset $s$ in a complete lattice $\alpha$, the infimum of the set $\{a\} \cup s$ is equal to the meet of $a$ and the infimum of $s$, i.e., $\bigwedge (\{a\} \cup s) = a \sqcap \bigwedge s$.

sSup_le_sSup_of_subset_insert_bot theorem

(h : s ⊆ insert ⊥ t) : sSup s ≤ sSup t

Full source

theorem sSup_le_sSup_of_subset_insert_bot (h : s ⊆ insert ⊥ t) : sSup s ≤ sSup t :=
  (sSup_le_sSup h).trans_eq (sSup_insert.trans (bot_sup_eq _))

Supremum Comparison for Sets with Bottom Element: $\bigvee s \leq \bigvee t$ when $s \subseteq t \cup \{\bot\}$

Informal description

For any subsets $s$ and $t$ of a complete lattice $\alpha$ with bottom element $\bot$, if $s$ is contained in $t \cup \{\bot\}$, then the supremum of $s$ is less than or equal to the supremum of $t$, i.e., \[ \bigvee s \leq \bigvee t. \]

sInf_le_sInf_of_subset_insert_top theorem

(h : s ⊆ insert ⊤ t) : sInf t ≤ sInf s

Full source

theorem sInf_le_sInf_of_subset_insert_top (h : s ⊆ insert ⊤ t) : sInf t ≤ sInf s :=
  (sInf_le_sInf h).trans_eq' (sInf_insert.trans (top_inf_eq _)).symm

Infimum Comparison under Top Insertion: $\bigwedge t \leq \bigwedge s$ when $s \subseteq t \cup \{\top\}$

Informal description

For any subsets $s$ and $t$ in a complete lattice $\alpha$, if $s$ is contained in the set obtained by inserting the top element $\top$ into $t$, then the infimum of $t$ is less than or equal to the infimum of $s$, i.e., $\bigwedge t \leq \bigwedge s$.

sSup_diff_singleton_bot theorem

(s : Set α) : sSup (s \ {⊥}) = sSup s

Full source

@[simp]
theorem sSup_diff_singleton_bot (s : Set α) : sSup (s \ {⊥}) = sSup s :=
  (sSup_le_sSup diff_subset).antisymm <|
    sSup_le_sSup_of_subset_insert_bot <| subset_insert_diff_singleton _ _

Supremum Invariance under Removal of Bottom Element: $\bigvee (s \setminus \{\bot\}) = \bigvee s$

Informal description

For any subset $s$ of a complete lattice $\alpha$ with a bottom element $\bot$, the supremum of the set difference $s \setminus \{\bot\}$ is equal to the supremum of $s$, i.e., \[ \bigvee (s \setminus \{\bot\}) = \bigvee s. \]

sInf_diff_singleton_top theorem

(s : Set α) : sInf (s \ {⊤}) = sInf s

Full source

@[simp]
theorem sInf_diff_singleton_top (s : Set α) : sInf (s \ {⊤}) = sInf s :=
  @sSup_diff_singleton_bot αᵒᵈ _ s

Infimum Invariance under Removal of Top Element: $\bigwedge (s \setminus \{\top\}) = \bigwedge s$

Informal description

For any subset $s$ of a complete lattice $\alpha$ with a top element $\top$, the infimum of the set difference $s \setminus \{\top\}$ is equal to the infimum of $s$, i.e., \[ \bigwedge (s \setminus \{\top\}) = \bigwedge s. \]

sSup_pair theorem

{a b : α} : sSup { a, b } = a ⊔ b

Full source

theorem sSup_pair {a b : α} : sSup {a, b} = a ⊔ b :=
  (@isLUB_pair α _ a b).sSup_eq

Supremum of a Pair Equals Join: $\bigvee \{a, b\} = a \sqcup b$

Informal description

For any two elements $a$ and $b$ in a complete lattice $\alpha$, the supremum of the set $\{a, b\}$ is equal to the join $a \sqcup b$.

sInf_pair theorem

{a b : α} : sInf { a, b } = a ⊓ b

Full source

theorem sInf_pair {a b : α} : sInf {a, b} = a ⊓ b :=
  (@isGLB_pair α _ a b).sInf_eq

Infimum of a Pair Equals Their Meet: $\inf\{a, b\} = a \sqcap b$

Informal description

For any two elements $a$ and $b$ in a complete lattice $\alpha$, the infimum of the set $\{a, b\}$ is equal to the meet $a \sqcap b$.

sSup_eq_bot theorem

: sSup s = ⊥ ↔ ∀ a ∈ s, a = ⊥

Full source

@[simp]
theorem sSup_eq_bot : sSupsSup s = ⊥ ↔ ∀ a ∈ s, a = ⊥ :=
  ⟨fun h _ ha => bot_unique <| h ▸ le_sSup ha, fun h =>
    bot_unique <| sSup_le fun a ha => le_bot_iff.2 <| h a ha⟩

Characterization of Supremum as Bottom Element: $\bigvee s = \bot \leftrightarrow \forall a \in s, a = \bot$

Informal description

For any subset $s$ of a complete lattice with a bottom element $\bot$, the supremum of $s$ equals $\bot$ if and only if every element $a \in s$ equals $\bot$.

sInf_eq_top theorem

: sInf s = ⊤ ↔ ∀ a ∈ s, a = ⊤

Full source

@[simp]
theorem sInf_eq_top : sInfsInf s = ⊤ ↔ ∀ a ∈ s, a = ⊤ :=
  @sSup_eq_bot αᵒᵈ _ _

Characterization of Infimum as Top Element: $\bigwedge s = \top \leftrightarrow \forall a \in s, a = \top$

Informal description

For any subset $s$ of a complete lattice with a top element $\top$, the infimum of $s$ equals $\top$ if and only if every element $a \in s$ equals $\top$.

sSup_eq_bot' theorem

{s : Set α} : sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}

Full source

lemma sSup_eq_bot' {s : Set α} : sSupsSup s = ⊥ ↔ s = ∅ ∨ s = {⊥} := by
  rw [sSup_eq_bot, ← subset_singleton_iff_eq, subset_singleton_iff]

Supremum Characterization for Bottom Element: $\bigvee s = \bot \leftrightarrow s = \emptyset \lor s = \{\bot\}$

Informal description

For any subset $s$ of a complete lattice with a bottom element $\bot$, the supremum of $s$ equals $\bot$ if and only if $s$ is either the empty set or the singleton set $\{\bot\}$.

sSup_eq_of_forall_le_of_forall_lt_exists_gt theorem

(h₁ : ∀ a ∈ s, a ≤ b) (h₂ : ∀ w, w < b → ∃ a ∈ s, w < a) : sSup s = b

Full source

/-- 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 sSup_eq_of_forall_le_of_forall_lt_exists_gt (h₁ : ∀ a ∈ s, a ≤ b)
    (h₂ : ∀ w, w < b → ∃ a ∈ s, w < a) : sSup s = b :=
  (sSup_le h₁).eq_of_not_lt fun h =>
    let ⟨_, ha, ha'⟩ := h₂ _ h
    ((le_sSup ha).trans_lt ha').false

Characterization of supremum via upper bounds and strict lower bounds

Informal description

Let $s$ be a subset of a complete lattice and $b$ an element. If every element $a \in s$ satisfies $a \leq b$, and for every $w < b$ there exists an element $a \in s$ such that $w < a$, then the supremum of $s$ is equal to $b$, i.e., $\bigvee s = b$.

sInf_eq_of_forall_ge_of_forall_gt_exists_lt theorem

: (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b

Full source

/-- 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 sInf_eq_of_forall_ge_of_forall_gt_exists_lt :
    (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b :=
  @sSup_eq_of_forall_le_of_forall_lt_exists_gt αᵒᵈ _ _ _

Characterization of infimum via lower bounds and strict upper bounds

Informal description

Let $s$ be a subset of a complete lattice and $b$ an element. If every element $a \in s$ satisfies $b \leq a$, and for every $w > b$ there exists an element $a \in s$ such that $a < w$, then the infimum of $s$ is equal to $b$, i.e., $\bigwedge s = b$.

sSup_range theorem

: sSup (range f) = iSup f

Full source

theorem sSup_range : sSup (range f) = iSup f :=
  rfl

Supremum of Range Equals Indexed Supremum

Informal description

For any function $f : \iota \to \alpha$ where $\alpha$ is a complete lattice, the supremum of the range of $f$ is equal to the indexed supremum of $f$, i.e., \[ \mathrm{sSup}(\mathrm{range}\, f) = \bigsqcup_i f(i). \]

sSup_eq_iSup' theorem

(s : Set α) : sSup s = ⨆ a : s, (a : α)

Full source

theorem sSup_eq_iSup' (s : Set α) : sSup s = ⨆ a : s, (a : α) := by rw [iSup, Subtype.range_coe]

Supremum as Indexed Supremum over Subset Elements

Informal description

For any subset $s$ of a complete lattice $\alpha$, the supremum of $s$ is equal to the indexed supremum of the canonical inclusion map from $s$ to $\alpha$, i.e., \[ \mathrm{sSup}(s) = \bigsqcup_{a \in s} a. \]

iSup_congr theorem

(h : ∀ i, f i = g i) : ⨆ i, f i = ⨆ i, g i

Full source

theorem iSup_congr (h : ∀ i, f i = g i) : ⨆ i, f i = ⨆ i, g i :=
  congr_arg _ <| funext h

Supremum Equality under Pointwise Equality

Informal description

For any indexed families of elements $f$ and $g$ in a complete lattice, if $f(i) = g(i)$ for all indices $i$, then their suprema are equal, i.e., $\bigsqcup_i f(i) = \bigsqcup_i g(i)$.

biSup_congr theorem

{p : ι → Prop} (h : ∀ i, p i → f i = g i) : ⨆ (i) (_ : p i), f i = ⨆ (i) (_ : p i), g i

Full source

theorem biSup_congr {p : ι → Prop} (h : ∀ i, p i → f i = g i) :
    ⨆ (i) (_ : p i), f i = ⨆ (i) (_ : p i), g i :=
  iSup_congr fun i ↦ iSup_congr (h i)

Bounded Supremum Equality under Pointwise Equality

Informal description

Let $p : \iota \to \mathrm{Prop}$ be a predicate and $f, g : \iota \to \alpha$ be two families of elements in a complete lattice $\alpha$. If for every index $i$ where $p(i)$ holds, we have $f(i) = g(i)$, then the bounded supremum $\bigsqcup_{i, p(i)} f(i)$ equals $\bigsqcup_{i, p(i)} g(i)$.

biSup_congr' theorem

 {p : ι → Prop} {f g : (i : ι) → p i → α} (h : ∀ i (hi : p i), f i hi = g i hi) :
  ⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi

Full source

theorem biSup_congr' {p : ι → Prop} {f g : (i : ι) → p i → α}
    (h : ∀ i (hi : p i), f i hi = g i hi) :
    ⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi := by
  congr; ext i; congr; ext hi; exact h i hi

Nested Supremum Equality under Pointwise Equality of Bounded Families

Informal description

Let $p : \iota \to \mathrm{Prop}$ be a predicate and $f, g : (i : \iota) \to p(i) \to \alpha$ be two families of elements in a complete lattice $\alpha$. If for every $i$ and every proof $h_i$ that $p(i)$ holds, we have $f(i, h_i) = g(i, h_i)$, then the supremum of the nested family $\bigsqcup_i \bigsqcup_{h_i : p(i)} f(i, h_i)$ equals the supremum of $\bigsqcup_i \bigsqcup_{h_i : p(i)} g(i, h_i)$.

Function.Surjective.iSup_comp theorem

{f : ι → ι'} (hf : Surjective f) (g : ι' → α) : ⨆ x, g (f x) = ⨆ y, g y

Full source

theorem Function.Surjective.iSup_comp {f : ι → ι'} (hf : Surjective f) (g : ι' → α) :
    ⨆ x, g (f x) = ⨆ y, g y := by
  simp only [iSup.eq_1]
  congr
  exact hf.range_comp g

Supremum Preservation under Composition with Surjective Function

Informal description

Let $f : \iota \to \iota'$ be a surjective function and $g : \iota' \to \alpha$ be any function into a complete lattice $\alpha$. Then the supremum of $g \circ f$ over $\iota$ equals the supremum of $g$ over $\iota'$, i.e., \[ \bigsqcup_{x \in \iota} g(f(x)) = \bigsqcup_{y \in \iota'} g(y). \]

Equiv.iSup_comp theorem

{g : ι' → α} (e : ι ≃ ι') : ⨆ x, g (e x) = ⨆ y, g y

Full source

theorem Equiv.iSup_comp {g : ι' → α} (e : ι ≃ ι') : ⨆ x, g (e x) = ⨆ y, g y :=
  e.surjective.iSup_comp _

Supremum Preservation under Composition with Equivalence

Informal description

Let $e : \iota \simeq \iota'$ be an equivalence between types $\iota$ and $\iota'$, and let $g : \iota' \to \alpha$ be a function into a complete lattice $\alpha$. Then the supremum of $g \circ e$ over $\iota$ equals the supremum of $g$ over $\iota'$, i.e., \[ \bigsqcup_{x \in \iota} g(e(x)) = \bigsqcup_{y \in \iota'} g(y). \]

Function.Surjective.iSup_congr theorem

{g : ι' → α} (h : ι → ι') (h1 : Surjective h) (h2 : ∀ x, g (h x) = f x) : ⨆ x, f x = ⨆ y, g y

Full source

protected theorem Function.Surjective.iSup_congr {g : ι' → α} (h : ι → ι') (h1 : Surjective h)
    (h2 : ∀ x, g (h x) = f x) : ⨆ x, f x = ⨆ y, g y := by
  convert h1.iSup_comp g
  exact (h2 _).symm

Supremum Equality under Surjective Function and Pointwise Equality

Informal description

Let $h : \iota \to \iota'$ be a surjective function, and let $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ be functions into a complete lattice $\alpha$. If for every $x \in \iota$, we have $g(h(x)) = f(x)$, then the suprema of $f$ and $g$ are equal, i.e., \[ \bigsqcup_{x \in \iota} f(x) = \bigsqcup_{y \in \iota'} g(y). \]

Equiv.iSup_congr theorem

{g : ι' → α} (e : ι ≃ ι') (h : ∀ x, g (e x) = f x) : ⨆ x, f x = ⨆ y, g y

Full source

protected theorem Equiv.iSup_congr {g : ι' → α} (e : ι ≃ ι') (h : ∀ x, g (e x) = f x) :
    ⨆ x, f x = ⨆ y, g y :=
  e.surjective.iSup_congr _ h

Supremum Equality under Type Equivalence and Pointwise Equality

Informal description

Let $e : \iota \simeq \iota'$ be an equivalence between types $\iota$ and $\iota'$, and let $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ be functions into a complete lattice $\alpha$. If for every $x \in \iota$, we have $g(e(x)) = f(x)$, then the suprema of $f$ and $g$ are equal, i.e., \[ \bigsqcup_{x \in \iota} f(x) = \bigsqcup_{y \in \iota'} g(y). \]

iSup_congr_Prop theorem

 {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q) (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iSup f₁ = iSup f₂

Full source

@[congr]
theorem iSup_congr_Prop {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q)
    (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iSup f₁ = iSup f₂ := by
  obtain rfl := propext pq
  congr with x
  apply f

Supremum Equality under Propositional Equivalence

Informal description

Let $p$ and $q$ be propositions, and let $f_1 : p \to \alpha$ and $f_2 : q \to \alpha$ be functions into a complete lattice $\alpha$. If $p$ and $q$ are logically equivalent (i.e., $p \leftrightarrow q$), and for every $x \in q$ we have $f_1(\text{pq.mpr } x) = f_2(x)$ where $\text{pq.mpr}$ is the implication $q \to p$, then the suprema of $f_1$ and $f_2$ are equal, i.e., $\bigsqcup f_1 = \bigsqcup f_2$.

iSup_plift_up theorem

(f : PLift ι → α) : ⨆ i, f (PLift.up i) = ⨆ i, f i

Full source

theorem iSup_plift_up (f : PLift ι → α) : ⨆ i, f (PLift.up i) = ⨆ i, f i :=
  (PLift.up_surjective.iSup_congr _) fun _ => rfl

Supremum Equality under Lifting: $\bigsqcup_i f(\mathrm{up}\,i) = \bigsqcup_i f(i)$

Informal description

For any function $f : \mathrm{PLift}\,\iota \to \alpha$ mapping from the lifted type to a complete lattice $\alpha$, the supremum of $f$ over the lifted indices equals the supremum of $f$ composed with the lifting function $\mathrm{PLift.up} : \iota \to \mathrm{PLift}\,\iota$. That is, \[ \bigsqcup_{i \in \iota} f(\mathrm{up}\,i) = \bigsqcup_{i \in \mathrm{PLift}\,\iota} f(i). \]

iSup_plift_down theorem

(f : ι → α) : ⨆ i, f (PLift.down i) = ⨆ i, f i

Full source

theorem iSup_plift_down (f : ι → α) : ⨆ i, f (PLift.down i) = ⨆ i, f i :=
  (PLift.down_surjective.iSup_congr _) fun _ => rfl

Supremum Invariance under PLift.down: $\bigsqcup_i f(i) = \bigsqcup_i f(\mathrm{down}\,i)$

Informal description

For any function $f : \iota \to \alpha$ mapping into a complete lattice $\alpha$, the supremum of $f$ over its domain $\iota$ is equal to the supremum of $f \circ \mathrm{PLift.down}$ over the lifted domain $\mathrm{PLift}\,\iota$, i.e., \[ \bigsqcup_{i \in \iota} f(i) = \bigsqcup_{i \in \mathrm{PLift}\,\iota} f(\mathrm{down}\,i). \]

iSup_range' theorem

(g : β → α) (f : ι → β) : ⨆ b : range f, g b = ⨆ i, g (f i)

Full source

theorem iSup_range' (g : β → α) (f : ι → β) : ⨆ b : range f, g b = ⨆ i, g (f i) := by
  rw [iSup, iSup, ← image_eq_range, ← range_comp']

Supremum over Range Equals Supremum of Composition: $\bigsqcup_{\mathrm{range}(f)} g = \bigsqcup_i g(f(i))$

Informal description

For any functions $g : \beta \to \alpha$ and $f : \iota \to \beta$, the supremum of $g$ over the range of $f$ equals the supremum of $g \circ f$ over the index set $\iota$, i.e., $$\bigsqcup_{b \in \mathrm{range}(f)} g(b) = \bigsqcup_{i \in \iota} g(f(i)).$$

sSup_image' theorem

{s : Set β} {f : β → α} : sSup (f '' s) = ⨆ a : s, f a

Full source

theorem sSup_image' {s : Set β} {f : β → α} : sSup (f '' s) = ⨆ a : s, f a := by
  rw [iSup, image_eq_range]

Supremum of Image Equals Indexed Supremum over Set Elements

Informal description

For any set $s \subseteq \beta$ and any function $f : \beta \to \alpha$, the supremum of the image of $s$ under $f$ equals the indexed supremum of $f$ over the elements of $s$, i.e., $$\mathrm{sSup}(f(s)) = \bigsqcup_{a \in s} f(a).$$

sInf_range theorem

: sInf (range f) = iInf f

Full source

theorem sInf_range : sInf (range f) = iInf f :=
  rfl

Infimum of Range Equals Indexed Infimum

Informal description

For any function $f : \iota \to \alpha$ where $\alpha$ has an infimum structure, the infimum of the range of $f$ equals the indexed infimum of $f$, i.e., $\mathrm{sInf}(\mathrm{range}\, f) = \bigsqcap_i f_i$.

sInf_eq_iInf' theorem

(s : Set α) : sInf s = ⨅ a : s, (a : α)

Full source

theorem sInf_eq_iInf' (s : Set α) : sInf s = ⨅ a : s, (a : α) :=
  @sSup_eq_iSup' αᵒᵈ _ _

Infimum as Indexed Infimum over Subset Elements

Informal description

For any subset $s$ of a complete lattice $\alpha$, the infimum of $s$ is equal to the indexed infimum of the canonical inclusion map from $s$ to $\alpha$, i.e., \[ \mathrm{sInf}(s) = \bigsqcap_{a \in s} a. \]

iInf_congr theorem

(h : ∀ i, f i = g i) : ⨅ i, f i = ⨅ i, g i

Full source

theorem iInf_congr (h : ∀ i, f i = g i) : ⨅ i, f i = ⨅ i, g i :=
  congr_arg _ <| funext h

Indexed Infimum Congruence: $\bigsqcap_i f_i = \bigsqcap_i g_i$ when $f_i = g_i$ for all $i$

Informal description

For any indexed families of elements $f$ and $g$ in a complete lattice, if $f_i = g_i$ for all indices $i$, then the infima of the families are equal, i.e., $\bigsqcap_i f_i = \bigsqcap_i g_i$.

biInf_congr theorem

{p : ι → Prop} (h : ∀ i, p i → f i = g i) : ⨅ (i) (_ : p i), f i = ⨅ (i) (_ : p i), g i

Full source

theorem biInf_congr {p : ι → Prop} (h : ∀ i, p i → f i = g i) :
    ⨅ (i) (_ : p i), f i = ⨅ (i) (_ : p i), g i :=
  biSup_congr (α := αᵒᵈ) h

Bounded Infimum Equality under Pointwise Equality

Informal description

Let $p : \iota \to \mathrm{Prop}$ be a predicate and $f, g : \iota \to \alpha$ be two families of elements in a complete lattice $\alpha$. If for every index $i$ where $p(i)$ holds, we have $f(i) = g(i)$, then the bounded infima are equal: \[ \bigsqcap_{i, p(i)} f(i) = \bigsqcap_{i, p(i)} g(i). \]

biInf_congr' theorem

 {p : ι → Prop} {f g : (i : ι) → p i → α} (h : ∀ i (hi : p i), f i hi = g i hi) :
  ⨅ i, ⨅ (hi : p i), f i hi = ⨅ i, ⨅ (hi : p i), g i hi

Full source

theorem biInf_congr' {p : ι → Prop} {f g : (i : ι) → p i → α}
    (h : ∀ i (hi : p i), f i hi = g i hi) :
    ⨅ i, ⨅ (hi : p i), f i hi = ⨅ i, ⨅ (hi : p i), g i hi := by
  congr; ext i; congr; ext hi; exact h i hi

Double Infimum Congruence under Pointwise Equality

Informal description

Let $p : \iota \to \mathrm{Prop}$ be a predicate and $f, g : (i : \iota) \to p(i) \to \alpha$ be two families of elements in a complete lattice $\alpha$. If for every $i$ and every proof $h_i$ that $p(i)$ holds, we have $f(i, h_i) = g(i, h_i)$, then the double infima are equal: \[ \bigsqcap_{i} \bigsqcap_{h_i : p(i)} f(i, h_i) = \bigsqcap_{i} \bigsqcap_{h_i : p(i)} g(i, h_i). \]

Function.Surjective.iInf_comp theorem

{f : ι → ι'} (hf : Surjective f) (g : ι' → α) : ⨅ x, g (f x) = ⨅ y, g y

Full source

theorem Function.Surjective.iInf_comp {f : ι → ι'} (hf : Surjective f) (g : ι' → α) :
    ⨅ x, g (f x) = ⨅ y, g y :=
  @Function.Surjective.iSup_comp αᵒᵈ _ _ _ f hf g

Infimum Preservation under Composition with Surjective Function

Informal description

Let $f : \iota \to \iota'$ be a surjective function and $g : \iota' \to \alpha$ be any function into a complete lattice $\alpha$. Then the infimum of $g \circ f$ over $\iota$ equals the infimum of $g$ over $\iota'$, i.e., \[ \bigsqcap_{x \in \iota} g(f(x)) = \bigsqcap_{y \in \iota'} g(y). \]

Equiv.iInf_comp theorem

{g : ι' → α} (e : ι ≃ ι') : ⨅ x, g (e x) = ⨅ y, g y

Full source

theorem Equiv.iInf_comp {g : ι' → α} (e : ι ≃ ι') : ⨅ x, g (e x) = ⨅ y, g y :=
  @Equiv.iSup_comp αᵒᵈ _ _ _ _ e

Infimum Preservation under Composition with Equivalence

Informal description

Let $e : \iota \simeq \iota'$ be an equivalence between types $\iota$ and $\iota'$, and let $g : \iota' \to \alpha$ be a function into a complete lattice $\alpha$. Then the infimum of $g \circ e$ over $\iota$ equals the infimum of $g$ over $\iota'$, i.e., \[ \bigsqcap_{x \in \iota} g(e(x)) = \bigsqcap_{y \in \iota'} g(y). \]

Function.Surjective.iInf_congr theorem

{g : ι' → α} (h : ι → ι') (h1 : Surjective h) (h2 : ∀ x, g (h x) = f x) : ⨅ x, f x = ⨅ y, g y

Full source

protected theorem Function.Surjective.iInf_congr {g : ι' → α} (h : ι → ι') (h1 : Surjective h)
    (h2 : ∀ x, g (h x) = f x) : ⨅ x, f x = ⨅ y, g y :=
  @Function.Surjective.iSup_congr αᵒᵈ _ _ _ _ _ h h1 h2

Infimum Equality under Surjective Function and Pointwise Equality

Informal description

Let $h : \iota \to \iota'$ be a surjective function, and let $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ be functions into a complete lattice $\alpha$. If for every $x \in \iota$, we have $g(h(x)) = f(x)$, then the infima of $f$ and $g$ are equal, i.e., \[ \bigsqcap_{x \in \iota} f(x) = \bigsqcap_{y \in \iota'} g(y). \]

Equiv.iInf_congr theorem

{g : ι' → α} (e : ι ≃ ι') (h : ∀ x, g (e x) = f x) : ⨅ x, f x = ⨅ y, g y

Full source

protected theorem Equiv.iInf_congr {g : ι' → α} (e : ι ≃ ι') (h : ∀ x, g (e x) = f x) :
    ⨅ x, f x = ⨅ y, g y :=
  @Equiv.iSup_congr αᵒᵈ _ _ _ _ _ e h

Infimum Equality under Type Equivalence and Pointwise Equality

Informal description

Let $\alpha$ be a complete lattice, and let $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ be functions. Given an equivalence $e : \iota \simeq \iota'$ such that for all $x \in \iota$, $g(e(x)) = f(x)$, then the infima of $f$ and $g$ are equal: \[ \bigsqcap_{x \in \iota} f(x) = \bigsqcap_{y \in \iota'} g(y). \]

iInf_congr_Prop theorem

 {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q) (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iInf f₁ = iInf f₂

Full source

@[congr]
theorem iInf_congr_Prop {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q)
    (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iInf f₁ = iInf f₂ :=
  @iSup_congr_Prop αᵒᵈ _ p q f₁ f₂ pq f

Infimum Equality under Propositional Equivalence

Informal description

Let $p$ and $q$ be propositions, and let $f_1 : p \to \alpha$ and $f_2 : q \to \alpha$ be functions into a complete lattice $\alpha$. If $p$ and $q$ are logically equivalent (i.e., $p \leftrightarrow q$), and for every $x \in q$ we have $f_1(\text{pq.mpr } x) = f_2(x)$ where $\text{pq.mpr}$ is the implication $q \to p$, then the infima of $f_1$ and $f_2$ are equal, i.e., $\bigsqcap f_1 = \bigsqcap f_2$.

iInf_plift_up theorem

(f : PLift ι → α) : ⨅ i, f (PLift.up i) = ⨅ i, f i

Full source

theorem iInf_plift_up (f : PLift ι → α) : ⨅ i, f (PLift.up i) = ⨅ i, f i :=
  (PLift.up_surjective.iInf_congr _) fun _ => rfl

Infimum Equality under PLift.up: $\bigsqcap_i f(\mathrm{up}\,i) = \bigsqcap_i f(i)$

Informal description

For any function $f : \mathrm{PLift}\,\iota \to \alpha$ from the lifted type $\mathrm{PLift}\,\iota$ to a complete lattice $\alpha$, the infimum of $f$ over the lifted indices equals the infimum of $f$ over the original indices. That is, \[ \bigsqcap_{i \in \iota} f(\mathrm{up}\,i) = \bigsqcap_{i \in \mathrm{PLift}\,\iota} f(i). \]

iInf_plift_down theorem

(f : ι → α) : ⨅ i, f (PLift.down i) = ⨅ i, f i

Full source

theorem iInf_plift_down (f : ι → α) : ⨅ i, f (PLift.down i) = ⨅ i, f i :=
  (PLift.down_surjective.iInf_congr _) fun _ => rfl

Infimum Invariance under PLift.down: $\bigsqcap_i f(i) = \bigsqcap_i f(\mathrm{down}\,i)$

Informal description

For any function $f \colon \iota \to \alpha$ mapping into a complete lattice $\alpha$, the infimum of $f$ over its domain $\iota$ is equal to the infimum of $f \circ \mathrm{PLift.down}$ over the lifted domain $\mathrm{PLift}\,\iota$. That is, \[ \bigsqcap_{i \in \iota} f(i) = \bigsqcap_{i \in \mathrm{PLift}\,\iota} f(\mathrm{down}\,i). \]

iInf_range' theorem

(g : β → α) (f : ι → β) : ⨅ b : range f, g b = ⨅ i, g (f i)

Full source

theorem iInf_range' (g : β → α) (f : ι → β) : ⨅ b : range f, g b = ⨅ i, g (f i) :=
  @iSup_range' αᵒᵈ _ _ _ _ _

Infimum over Range Equals Infimum of Composition: $\bigsqcap_{\mathrm{range}(f)} g = \bigsqcap_i g(f(i))$

Informal description

For any function $g : \beta \to \alpha$ and any function $f : \iota \to \beta$, the infimum of $g$ over the range of $f$ equals the infimum of the composition $g \circ f$ over the index set $\iota$, i.e., $$\bigsqcap_{b \in \mathrm{range}(f)} g(b) = \bigsqcap_{i \in \iota} g(f(i)).$$

sInf_image' theorem

{s : Set β} {f : β → α} : sInf (f '' s) = ⨅ a : s, f a

Full source

theorem sInf_image' {s : Set β} {f : β → α} : sInf (f '' s) = ⨅ a : s, f a :=
  @sSup_image' αᵒᵈ _ _ _ _

Infimum of Image Equals Indexed Infimum over Set Elements

Informal description

For any set $s \subseteq \beta$ and any function $f \colon \beta \to \alpha$, the infimum of the image of $s$ under $f$ equals the indexed infimum of $f$ over the elements of $s$, i.e., $$\mathrm{sInf}(f(s)) = \bigsqcap_{a \in s} f(a).$$

le_iSup theorem

(f : ι → α) (i : ι) : f i ≤ iSup f

Full source

theorem le_iSup (f : ι → α) (i : ι) : f i ≤ iSup f :=
  le_sSup ⟨i, rfl⟩

Element is Less Than or Equal to Supremum: $f(i) \leq \bigsqcup_i f(i)$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$ and any index $i \in \iota$, the element $f(i)$ is less than or equal to the supremum of $f$, i.e., $f(i) \leq \bigsqcup_i f(i)$.

iInf_le theorem

(f : ι → α) (i : ι) : iInf f ≤ f i

Full source

theorem iInf_le (f : ι → α) (i : ι) : iInf f ≤ f i :=
  sInf_le ⟨i, rfl⟩

Infimum is a Lower Bound: $\bigsqcap_i f(i) \leq f(i)$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$ and any index $i \in \iota$, the infimum of $f$ is less than or equal to $f(i)$, i.e., $\bigsqcap_i f(i) \leq f(i)$.

iInf_le_iSup theorem

[Nonempty ι] : ⨅ i, f i ≤ ⨆ i, f i

Full source

lemma iInf_le_iSup [Nonempty ι] : ⨅ i, f i ≤ ⨆ i, f i :=
  (iInf_le _ (Classical.arbitrary _)).trans <| le_iSup _ (Classical.arbitrary _)

Infimum is Less Than or Equal to Supremum in Complete Lattices

Informal description

For any nonempty index type $\iota$ and any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$, the infimum of $f$ is less than or equal to the supremum of $f$, i.e., $\bigsqcap_i f(i) \leq \bigsqcup_i f(i)$.

le_iSup' theorem

(f : ι → α) (i : ι) : f i ≤ iSup f

Full source

@[deprecated le_iSup (since := "2024-12-13")]
theorem le_iSup' (f : ι → α) (i : ι) : f i ≤ iSup f := le_iSup f i

Element is bounded by supremum: $f(i) \leq \bigsqcup_i f(i)$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$ and any index $i \in \iota$, the element $f(i)$ is less than or equal to the supremum of $f$, i.e., $f(i) \leq \bigsqcup_i f(i)$.

iInf_le' theorem

(f : ι → α) (i : ι) : iInf f ≤ f i

Full source

@[deprecated iInf_le (since := "2024-12-13")]
theorem iInf_le' (f : ι → α) (i : ι) : iInf f ≤ f i := iInf_le f i

Infimum is a Lower Bound: $\bigsqcap_i f(i) \leq f(i)$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$ and any index $i \in \iota$, the infimum of $f$ is less than or equal to $f(i)$, i.e., $\bigsqcap_i f(i) \leq f(i)$.

isLUB_iSup theorem

: IsLUB (range f) (⨆ j, f j)

Full source

theorem isLUB_iSup : IsLUB (range f) (⨆ j, f j) :=
  isLUB_sSup _

Indexed Supremum is Least Upper Bound of Range

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$, the indexed supremum $\bigsqcup_{j} f(j)$ is the least upper bound of the range of $f$. That is, $\bigsqcup_{j} f(j)$ is an upper bound for $\{f(j) \mid j \in \iota\}$ and is less than or equal to any other upper bound of this set.

isGLB_iInf theorem

: IsGLB (range f) (⨅ j, f j)

Full source

theorem isGLB_iInf : IsGLB (range f) (⨅ j, f j) :=
  isGLB_sInf _

Indexed Infimum is Greatest Lower Bound of Range: $\bigsqcap_j f_j = \text{GLB}(\text{range}\, f)$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$, the indexed infimum $\bigsqcap_{j} f_j$ is the greatest lower bound of the range of $f$. That is, $\bigsqcap_{j} f_j$ is a lower bound for $\{f_j \mid j \in \iota\}$ and is greater than or equal to any other lower bound of this set.

IsLUB.iSup_eq theorem

(h : IsLUB (range f) a) : ⨆ j, f j = a

Full source

theorem IsLUB.iSup_eq (h : IsLUB (range f) a) : ⨆ j, f j = a :=
  h.sSup_eq

Supremum Characterization via Least Upper Bound: $\bigsqcup_j f_j = a$ when $a$ is the least upper bound of $\text{range}\, f$

Informal description

Let $f : \iota \to \alpha$ be an indexed family of elements in a complete lattice $\alpha$, and let $a \in \alpha$. If $a$ is the least upper bound of the range of $f$ (i.e., $a$ is an upper bound for $\{f(j) \mid j \in \iota\}$ and is less than or equal to any other upper bound of this set), then the indexed supremum of $f$ equals $a$, i.e., $\bigsqcup_j f(j) = a$.

IsGLB.iInf_eq theorem

(h : IsGLB (range f) a) : ⨅ j, f j = a

Full source

theorem IsGLB.iInf_eq (h : IsGLB (range f) a) : ⨅ j, f j = a :=
  h.sInf_eq

Greatest Lower Bound Characterizes Indexed Infimum: $\text{GLB}(\text{range}\, f) = a \Rightarrow \bigsqcap_j f_j = a$

Informal description

Let $f : \iota \to \alpha$ be an indexed family of elements in a complete lattice $\alpha$. If $a$ is the greatest lower bound of the range of $f$, then the indexed infimum $\bigsqcap_j f_j$ equals $a$.

le_iSup_of_le theorem

(i : ι) (h : a ≤ f i) : a ≤ iSup f

Full source

theorem le_iSup_of_le (i : ι) (h : a ≤ f i) : a ≤ iSup f :=
  h.trans <| le_iSup _ i

Element Below Indexed Family Member is Below Supremum: $a \leq f(i) \Rightarrow a \leq \bigsqcup_i f(i)$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$, if an element $a \in \alpha$ satisfies $a \leq f(i)$ for some index $i \in \iota$, then $a$ is less than or equal to the supremum of $f$, i.e., $a \leq \bigsqcup_i f(i)$.

iInf_le_of_le theorem

(i : ι) (h : f i ≤ a) : iInf f ≤ a

Full source

theorem iInf_le_of_le (i : ι) (h : f i ≤ a) : iInf f ≤ a :=
  (iInf_le _ i).trans h

Infimum is Below Any Upper Bound: $\bigsqcap_i f(i) \leq a$ when $f(i) \leq a$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$, if there exists an index $i \in \iota$ such that $f(i) \leq a$ for some $a \in \alpha$, then the infimum of $f$ satisfies $\bigsqcap_i f(i) \leq a$.

le_iSup₂ theorem

{f : ∀ i, κ i → α} (i : ι) (j : κ i) : f i j ≤ ⨆ (i) (j), f i j

Full source

theorem le_iSup₂ {f : ∀ i, κ i → α} (i : ι) (j : κ i) : f i j ≤ ⨆ (i) (j), f i j :=
  le_iSup_of_le i <| le_iSup (f i) j

Element is Less Than or Equal to Double Supremum: $f(i,j) \leq \bigsqcup_{i,j} f(i,j)$

Informal description

For any doubly indexed family of elements $f : \forall i, \kappa_i \to \alpha$ in a complete lattice $\alpha$, and for any indices $i \in \iota$ and $j \in \kappa_i$, the element $f(i,j)$ is less than or equal to the supremum $\bigsqcup_{i,j} f(i,j)$.

iInf₂_le theorem

{f : ∀ i, κ i → α} (i : ι) (j : κ i) : ⨅ (i) (j), f i j ≤ f i j

Full source

theorem iInf₂_le {f : ∀ i, κ i → α} (i : ι) (j : κ i) : ⨅ (i) (j), f i j ≤ f i j :=
  iInf_le_of_le i <| iInf_le (f i) j

Double Infimum is a Lower Bound: $\bigsqcap_{i,j} f(i,j) \leq f(i,j)$

Informal description

For any doubly indexed family of elements $f : \forall i, \kappa_i \to \alpha$ in a complete lattice $\alpha$ and any indices $i \in \iota$ and $j \in \kappa_i$, the double infimum satisfies $\bigsqcap_{i,j} f(i,j) \leq f(i,j)$.

le_iSup₂_of_le theorem

{f : ∀ i, κ i → α} (i : ι) (j : κ i) (h : a ≤ f i j) : a ≤ ⨆ (i) (j), f i j

Full source

theorem le_iSup₂_of_le {f : ∀ i, κ i → α} (i : ι) (j : κ i) (h : a ≤ f i j) :
    a ≤ ⨆ (i) (j), f i j :=
  h.trans <| le_iSup₂ i j

Element bounded by $f(i,j)$ is bounded by double supremum: $a \leq f(i,j) \implies a \leq \bigsqcup_{i,j} f(i,j)$

Informal description

For any doubly indexed family of elements $f : \forall i, \kappa_i \to \alpha$ in a complete lattice $\alpha$, if an element $a \in \alpha$ satisfies $a \leq f(i,j)$ for some indices $i \in \iota$ and $j \in \kappa_i$, then $a$ is less than or equal to the double supremum $\bigsqcup_{i,j} f(i,j)$.

iInf₂_le_of_le theorem

{f : ∀ i, κ i → α} (i : ι) (j : κ i) (h : f i j ≤ a) : ⨅ (i) (j), f i j ≤ a

Full source

theorem iInf₂_le_of_le {f : ∀ i, κ i → α} (i : ι) (j : κ i) (h : f i j ≤ a) :
    ⨅ (i) (j), f i j ≤ a :=
  (iInf₂_le i j).trans h

Double Infimum is Below Any Upper Bound: $\bigsqcap_{i,j} f(i,j) \leq a$ when $f(i,j) \leq a$

Informal description

For any doubly indexed family of elements $f : \forall i, \kappa_i \to \alpha$ in a complete lattice $\alpha$, if there exists indices $i \in \iota$ and $j \in \kappa_i$ such that $f(i,j) \leq a$ for some element $a \in \alpha$, then the double infimum satisfies $\bigsqcap_{i,j} f(i,j) \leq a$.

iSup_le theorem

(h : ∀ i, f i ≤ a) : iSup f ≤ a

Full source

theorem iSup_le (h : ∀ i, f i ≤ a) : iSup f ≤ a :=
  sSup_le fun _ ⟨i, Eq⟩ => Eq ▸ h i

Supremum is the least upper bound of an indexed family

Informal description

For any indexed family of elements $(f_i)_{i \in \iota}$ in a complete lattice $\alpha$ and any element $a \in \alpha$, if $f_i \leq a$ for all $i \in \iota$, then the supremum of the family satisfies $\bigsqcup_{i \in \iota} f_i \leq a$.

le_iInf theorem

(h : ∀ i, a ≤ f i) : a ≤ iInf f

Full source

theorem le_iInf (h : ∀ i, a ≤ f i) : a ≤ iInf f :=
  le_sInf fun _ ⟨i, Eq⟩ => Eq ▸ h i

Infimum is Greatest Lower Bound: $a \leq \bigsqcap_i f(i)$ for all lower bounds $a$ of $f$

Informal description

For any element $a$ in a complete lattice $\alpha$ and any indexed family of elements $f : \iota \to \alpha$, if $a$ is a lower bound for the family $f$ (i.e., $a \leq f(i)$ for all $i \in \iota$), then $a$ is less than or equal to the infimum of $f$, i.e., $a \leq \bigsqcap_i f(i)$.

iSup₂_le theorem

{f : ∀ i, κ i → α} (h : ∀ i j, f i j ≤ a) : ⨆ (i) (j), f i j ≤ a

Full source

theorem iSup₂_le {f : ∀ i, κ i → α} (h : ∀ i j, f i j ≤ a) : ⨆ (i) (j), f i j ≤ a :=
  iSup_le fun i => iSup_le <| h i

Double Supremum is Least Upper Bound: $\bigsqcup_{i,j} f_{i,j} \leq a$ for all upper bounds $a$ of $f$

Informal description

For any indexed family of elements $(f_{i,j})_{i \in \iota, j \in \kappa_i}$ in a complete lattice $\alpha$ and any element $a \in \alpha$, if $f_{i,j} \leq a$ for all $i \in \iota$ and $j \in \kappa_i$, then the double supremum satisfies $\bigsqcup_{i \in \iota} \bigsqcup_{j \in \kappa_i} f_{i,j} \leq a$.

le_iInf₂ theorem

{f : ∀ i, κ i → α} (h : ∀ i j, a ≤ f i j) : a ≤ ⨅ (i) (j), f i j

Full source

theorem le_iInf₂ {f : ∀ i, κ i → α} (h : ∀ i j, a ≤ f i j) : a ≤ ⨅ (i) (j), f i j :=
  le_iInf fun i => le_iInf <| h i

Infimum is Greatest Lower Bound for Doubly-Indexed Family: $a \leq \bigsqcap_{i,j} f(i,j)$ for all lower bounds $a$ of $f$

Informal description

For any element $a$ in a complete lattice $\alpha$ and any doubly-indexed family of elements $f : \forall i, \kappa_i \to \alpha$, if $a$ is a lower bound for the family $f$ (i.e., $a \leq f(i,j)$ for all $i$ and $j$), then $a$ is less than or equal to the infimum of $f$, i.e., $a \leq \bigsqcap_{i,j} f(i,j)$.

iSup₂_le_iSup theorem

(κ : ι → Sort*) (f : ι → α) : ⨆ (i) (_ : κ i), f i ≤ ⨆ i, f i

Full source

theorem iSup₂_le_iSup (κ : ι → Sort*) (f : ι → α) : ⨆ (i) (_ : κ i), f i ≤ ⨆ i, f i :=
  iSup₂_le fun i _ => le_iSup f i

Double Supremum is Bounded by Single Supremum: $\bigsqcup_{i,j} f(i) \leq \bigsqcup_i f(i)$

Informal description

For any indexed family of types $\kappa : \iota \to \text{Sort}^*$ and any family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$, the double supremum $\bigsqcup_{i \in \iota} \bigsqcup_{j \in \kappa_i} f(i)$ is less than or equal to the single supremum $\bigsqcup_{i \in \iota} f(i)$.

iInf_le_iInf₂ theorem

(κ : ι → Sort*) (f : ι → α) : ⨅ i, f i ≤ ⨅ (i) (_ : κ i), f i

Full source

theorem iInf_le_iInf₂ (κ : ι → Sort*) (f : ι → α) : ⨅ i, f i ≤ ⨅ (i) (_ : κ i), f i :=
  le_iInf₂ fun i _ => iInf_le f i

Infimum is Less Than or Equal to Doubly-Indexed Infimum: $\bigsqcap_i f(i) \leq \bigsqcap_{i,j} f(i)$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$ and any family of types $\kappa : \iota \to \text{Sort}$, the infimum of $f$ is less than or equal to the doubly-indexed infimum $\bigsqcap_{i, j} f(i)$, where $j$ ranges over $\kappa(i)$. In other words, $\bigsqcap_i f(i) \leq \bigsqcap_{i, j} f(i)$.

iSup_mono theorem

(h : ∀ i, f i ≤ g i) : iSup f ≤ iSup g

Full source

@[gcongr]
theorem iSup_mono (h : ∀ i, f i ≤ g i) : iSup f ≤ iSup g :=
  iSup_le fun i => le_iSup_of_le i <| h i

Monotonicity of Supremum: $f_i \leq g_i \Rightarrow \bigsqcup_i f_i \leq \bigsqcup_i g_i$

Informal description

For any indexed family of elements $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ in a complete lattice $\alpha$, if $f_i \leq g_i$ for all $i \in \iota$, then the supremum of the $f_i$ family is less than or equal to the supremum of the $g_i$ family, i.e., $\bigsqcup_i f_i \leq \bigsqcup_i g_i$.

iInf_mono theorem

(h : ∀ i, f i ≤ g i) : iInf f ≤ iInf g

Full source

@[gcongr]
theorem iInf_mono (h : ∀ i, f i ≤ g i) : iInf f ≤ iInf g :=
  le_iInf fun i => iInf_le_of_le i <| h i

Monotonicity of Infimum: $f(i) \leq g(i)$ implies $\bigsqcap_i f(i) \leq \bigsqcap_i g(i)$

Informal description

For any indexed family of elements $f, g : \iota \to \alpha$ in a complete lattice $\alpha$, if $f(i) \leq g(i)$ for all $i \in \iota$, then the infimum of $f$ is less than or equal to the infimum of $g$, i.e., $\bigsqcap_i f(i) \leq \bigsqcap_i g(i)$.

iSup₂_mono theorem

{f g : ∀ i, κ i → α} (h : ∀ i j, f i j ≤ g i j) : ⨆ (i) (j), f i j ≤ ⨆ (i) (j), g i j

Full source

theorem iSup₂_mono {f g : ∀ i, κ i → α} (h : ∀ i j, f i j ≤ g i j) :
    ⨆ (i) (j), f i j ≤ ⨆ (i) (j), g i j :=
  iSup_mono fun i => iSup_mono <| h i

Monotonicity of Double Supremum: $f_{i,j} \leq g_{i,j} \Rightarrow \bigsqcup_{i,j} f_{i,j} \leq \bigsqcup_{i,j} g_{i,j}$

Informal description

For any indexed families of elements $f, g : \forall i, \kappa i \to \alpha$ in a complete lattice $\alpha$, if $f(i)(j) \leq g(i)(j)$ for all $i$ and $j$, then the double supremum $\bigsqcup_{i,j} f(i)(j)$ is less than or equal to $\bigsqcup_{i,j} g(i)(j)$.

iInf₂_mono theorem

{f g : ∀ i, κ i → α} (h : ∀ i j, f i j ≤ g i j) : ⨅ (i) (j), f i j ≤ ⨅ (i) (j), g i j

Full source

theorem iInf₂_mono {f g : ∀ i, κ i → α} (h : ∀ i j, f i j ≤ g i j) :
    ⨅ (i) (j), f i j ≤ ⨅ (i) (j), g i j :=
  iInf_mono fun i => iInf_mono <| h i

Monotonicity of Double Infimum: $f(i,j) \leq g(i,j)$ implies $\bigsqcap_{i,j} f(i,j) \leq \bigsqcap_{i,j} g(i,j)$

Informal description

For any indexed families of elements $f, g : \forall i, \kappa_i \to \alpha$ in a complete lattice $\alpha$, if for every $i$ and $j$, $f(i, j) \leq g(i, j)$, then the double infimum satisfies $\bigsqcap_{i,j} f(i, j) \leq \bigsqcap_{i,j} g(i, j)$.

iSup_mono' theorem

{g : ι' → α} (h : ∀ i, ∃ i', f i ≤ g i') : iSup f ≤ iSup g

Full source

theorem iSup_mono' {g : ι' → α} (h : ∀ i, ∃ i', f i ≤ g i') : iSup f ≤ iSup g :=
  iSup_le fun i => Exists.elim (h i) le_iSup_of_le

Monotonicity of Supremum under Pointwise Comparison: $\forall i, \exists i', f(i) \leq g(i') \Rightarrow \bigsqcup_i f(i) \leq \bigsqcup_{i'} g(i')$

Informal description

Let $\alpha$ be a complete lattice, and let $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ be two indexed families of elements in $\alpha$. If for every index $i \in \iota$ there exists an index $i' \in \iota'$ such that $f(i) \leq g(i')$, then the supremum of $f$ is less than or equal to the supremum of $g$, i.e., $\bigsqcup_i f(i) \leq \bigsqcup_{i'} g(i')$.

iInf_mono' theorem

{g : ι' → α} (h : ∀ i', ∃ i, f i ≤ g i') : iInf f ≤ iInf g

Full source

theorem iInf_mono' {g : ι' → α} (h : ∀ i', ∃ i, f i ≤ g i') : iInf f ≤ iInf g :=
  le_iInf fun i' => Exists.elim (h i') iInf_le_of_le

Comparison of Infima under Pointwise Inequality: $\bigsqcap_i f(i) \leq \bigsqcap_{i'} g(i')$ when $f(i) \leq g(i')$ for some $i$ per $i'$

Informal description

For any indexed families of elements $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ in a complete lattice $\alpha$, if for every index $i' \in \iota'$ there exists an index $i \in \iota$ such that $f(i) \leq g(i')$, then the infimum of $f$ is less than or equal to the infimum of $g$, i.e., $\bigsqcap_i f(i) \leq \bigsqcap_{i'} g(i')$.

iSup₂_mono' theorem

 {f : ∀ i, κ i → α} {g : ∀ i', κ' i' → α} (h : ∀ i j, ∃ i' j', f i j ≤ g i' j') : ⨆ (i) (j), f i j ≤ ⨆ (i) (j), g i j

Full source

theorem iSup₂_mono' {f : ∀ i, κ i → α} {g : ∀ i', κ' i' → α} (h : ∀ i j, ∃ i' j', f i j ≤ g i' j') :
    ⨆ (i) (j), f i j ≤ ⨆ (i) (j), g i j :=
  iSup₂_le fun i j =>
    let ⟨i', j', h⟩ := h i j
    le_iSup₂_of_le i' j' h

Monotonicity of Double Supremum under Pointwise Comparison

Informal description

Let $\alpha$ be a complete lattice, and let $f : \forall i, \kappa_i \to \alpha$ and $g : \forall i', \kappa'_{i'} \to \alpha$ be two doubly indexed families of elements in $\alpha$. If for every $i \in \iota$ and $j \in \kappa_i$, there exist $i' \in \iota'$ and $j' \in \kappa'_{i'}$ such that $f(i,j) \leq g(i',j')$, then the double supremum satisfies \[ \bigsqcup_{i \in \iota} \bigsqcup_{j \in \kappa_i} f(i,j) \leq \bigsqcup_{i' \in \iota'} \bigsqcup_{j' \in \kappa'_{i'}} g(i',j'). \]

iInf₂_mono' theorem

 {f : ∀ i, κ i → α} {g : ∀ i', κ' i' → α} (h : ∀ i j, ∃ i' j', f i' j' ≤ g i j) : ⨅ (i) (j), f i j ≤ ⨅ (i) (j), g i j

Full source

theorem iInf₂_mono' {f : ∀ i, κ i → α} {g : ∀ i', κ' i' → α} (h : ∀ i j, ∃ i' j', f i' j' ≤ g i j) :
    ⨅ (i) (j), f i j ≤ ⨅ (i) (j), g i j :=
  le_iInf₂ fun i j =>
    let ⟨i', j', h⟩ := h i j
    iInf₂_le_of_le i' j' h

Monotonicity of Double Infimum under Pointwise Inequality

Informal description

For any doubly indexed families of elements $f : \forall i, \kappa_i \to \alpha$ and $g : \forall i', \kappa'_{i'} \to \alpha$ in a complete lattice $\alpha$, if for every pair of indices $(i,j)$ there exists a pair $(i',j')$ such that $f(i',j') \leq g(i,j)$, then the double infimum of $f$ is less than or equal to the double infimum of $g$, i.e., \[ \bigsqcap_{i,j} f(i,j) \leq \bigsqcap_{i,j} g(i,j). \]

iSup_const_mono theorem

(h : ι → ι') : ⨆ _ : ι, a ≤ ⨆ _ : ι', a

Full source

theorem iSup_const_mono (h : ι → ι') : ⨆ _ : ι, a ≤ ⨆ _ : ι', a :=
  iSup_le <| le_iSuple_iSup _ ∘ h

Monotonicity of Constant Supremum under Index Transformation

Informal description

For any function $h : \iota \to \iota'$ between index types, the supremum of a constant element $a$ over $\iota$ is less than or equal to the supremum of $a$ over $\iota'$, i.e., \[ \bigsqcup_{i \in \iota} a \leq \bigsqcup_{i' \in \iota'} a. \]

iInf_const_mono theorem

(h : ι' → ι) : ⨅ _ : ι, a ≤ ⨅ _ : ι', a

Full source

theorem iInf_const_mono (h : ι' → ι) : ⨅ _ : ι, a ≤ ⨅ _ : ι', a :=
  le_iInf <| iInf_leiInf_le _ ∘ h

Monotonicity of Infimum under Index Type Change: $\bigsqcap_\iota a \leq \bigsqcap_{\iota'} a$ for $h : \iota' \to \iota$

Informal description

For any complete lattice $\alpha$, any element $a \in \alpha$, and any pair of index types $\iota$ and $\iota'$ with a map $h : \iota' \to \iota$, the infimum of the constant family $a$ over $\iota$ is less than or equal to the infimum of the constant family $a$ over $\iota'$. In symbols: \[ \bigsqcap_{i \in \iota} a \leq \bigsqcap_{i' \in \iota'} a \]

iSup_iInf_le_iInf_iSup theorem

(f : ι → ι' → α) : ⨆ i, ⨅ j, f i j ≤ ⨅ j, ⨆ i, f i j

Full source

theorem iSup_iInf_le_iInf_iSup (f : ι → ι' → α) : ⨆ i, ⨅ j, f i j ≤ ⨅ j, ⨆ i, f i j :=
  iSup_le fun i => iInf_mono fun j => le_iSup (fun i => f i j) i

Inequality between Iterated Suprema and Infima: $\bigsqcup_i \bigsqcap_j f(i,j) \leq \bigsqcap_j \bigsqcup_i f(i,j)$

Informal description

For any complete lattice $\alpha$ and any doubly indexed family of elements $f : \iota \times \iota' \to \alpha$, the supremum over $i$ of the infimum over $j$ of $f(i,j)$ is less than or equal to the infimum over $j$ of the supremum over $i$ of $f(i,j)$. In symbols: \[ \bigsqcup_{i} \bigsqcap_{j} f(i,j) \leq \bigsqcap_{j} \bigsqcup_{i} f(i,j) \]

biSup_mono theorem

{p q : ι → Prop} (hpq : ∀ i, p i → q i) : ⨆ (i) (_ : p i), f i ≤ ⨆ (i) (_ : q i), f i

Full source

theorem biSup_mono {p q : ι → Prop} (hpq : ∀ i, p i → q i) :
    ⨆ (i) (_ : p i), f i ≤ ⨆ (i) (_ : q i), f i :=
  iSup_mono fun i => iSup_const_mono (hpq i)

Monotonicity of Bounded Supremum under Weakening of Predicate

Informal description

For any indexed family of elements $(f_i)_{i \in \iota}$ in a complete lattice $\alpha$ and any pair of predicates $p, q : \iota \to \text{Prop}$ such that $p(i)$ implies $q(i)$ for all $i \in \iota$, the bounded supremum over $i$ satisfying $p(i)$ is less than or equal to the bounded supremum over $i$ satisfying $q(i)$. In symbols: \[ \bigsqcup_{\substack{i \in \iota \\ p(i)}} f_i \leq \bigsqcup_{\substack{i \in \iota \\ q(i)}} f_i \]

biInf_mono theorem

{p q : ι → Prop} (hpq : ∀ i, p i → q i) : ⨅ (i) (_ : q i), f i ≤ ⨅ (i) (_ : p i), f i

Full source

theorem biInf_mono {p q : ι → Prop} (hpq : ∀ i, p i → q i) :
    ⨅ (i) (_ : q i), f i ≤ ⨅ (i) (_ : p i), f i :=
  iInf_mono fun i => iInf_const_mono (hpq i)

Monotonicity of Bounded Infimum: $p \subseteq q$ implies $\bigsqcap_{q(i)} f(i) \leq \bigsqcap_{p(i)} f(i)$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$ and any pair of predicates $p, q : \iota \to \text{Prop}$ such that for all $i$, $p(i)$ implies $q(i)$, the infimum of $f$ over the indices satisfying $q$ is less than or equal to the infimum of $f$ over the indices satisfying $p$. In symbols: \[ \bigsqcap_{i \in \iota, q(i)} f(i) \leq \bigsqcap_{i \in \iota, p(i)} f(i) \]

iSup_le_iff theorem

: iSup f ≤ a ↔ ∀ i, f i ≤ a

Full source

@[simp]
theorem iSup_le_iff : iSupiSup f ≤ a ↔ ∀ i, f i ≤ a :=
  (isLUB_le_iff isLUB_iSup).trans forall_mem_range

Supremum Comparison Criterion: $\bigsqcup_i f_i \leq a \leftrightarrow \forall i, f_i \leq a$

Informal description

For any indexed family of elements $f_i$ in a complete lattice $\alpha$, the supremum $\bigsqcup_i f_i$ is less than or equal to an element $a$ if and only if $f_i \leq a$ for every index $i$.

le_iInf_iff theorem

: a ≤ iInf f ↔ ∀ i, a ≤ f i

Full source

@[simp]
theorem le_iInf_iff : a ≤ iInf f ↔ ∀ i, a ≤ f i :=
  (le_isGLB_iff isGLB_iInf).trans forall_mem_range

Characterization of Infimum Inequality: $a \leq \bigsqcap_i f_i \leftrightarrow \forall i, a \leq f_i$

Informal description

For any element $a$ in a complete lattice $\alpha$ and any indexed family of elements $f : \iota \to \alpha$, the inequality $a \leq \bigsqcap_i f_i$ holds if and only if $a \leq f_i$ for all indices $i$.

iSup₂_le_iff theorem

{f : ∀ i, κ i → α} : ⨆ (i) (j), f i j ≤ a ↔ ∀ i j, f i j ≤ a

Full source

theorem iSup₂_le_iff {f : ∀ i, κ i → α} : ⨆ (i) (j), f i j⨆ (i) (j), f i j ≤ a ↔ ∀ i j, f i j ≤ a := by
  simp_rw [iSup_le_iff]

Characterization of Supremum of Double-Indexed Family in Complete Lattice

Informal description

For any indexed family of elements $f_{i,j}$ in a complete lattice $\alpha$, the supremum $\bigsqcup_{i,j} f_{i,j}$ is less than or equal to an element $a$ if and only if $f_{i,j} \leq a$ for all $i$ and $j$.

le_iInf₂_iff theorem

{f : ∀ i, κ i → α} : (a ≤ ⨅ (i) (j), f i j) ↔ ∀ i j, a ≤ f i j

Full source

theorem le_iInf₂_iff {f : ∀ i, κ i → α} : (a ≤ ⨅ (i) (j), f i j) ↔ ∀ i j, a ≤ f i j := by
  simp_rw [le_iInf_iff]

Characterization of Infimum Inequality for Doubly-Indexed Family

Informal description

For any element $a$ in a complete lattice $\alpha$ and any doubly-indexed family of elements $f : \forall i, \kappa_i \to \alpha$, the inequality $a \leq \bigsqcap_{i,j} f(i,j)$ holds if and only if for all indices $i$ and $j$, we have $a \leq f(i,j)$.

iSup_lt_iff theorem

: iSup f < a ↔ ∃ b, b < a ∧ ∀ i, f i ≤ b

Full source

theorem iSup_lt_iff : iSupiSup f < a ↔ ∃ b, b < a ∧ ∀ i, f i ≤ b :=
  ⟨fun h => ⟨iSup f, h, le_iSup f⟩, fun ⟨_, h, hb⟩ => (iSup_le hb).trans_lt h⟩

Characterization of Strict Supremum Inequality: $\bigsqcup_i f_i < a$

Informal description

For an indexed family of elements $(f_i)_{i \in \iota}$ in a complete lattice $\alpha$ and an element $a \in \alpha$, the supremum $\bigsqcup_i f_i$ is strictly less than $a$ if and only if there exists some element $b \in \alpha$ such that $b < a$ and $f_i \leq b$ for all $i \in \iota$.

lt_iInf_iff theorem

: a < iInf f ↔ ∃ b, a < b ∧ ∀ i, b ≤ f i

Full source

theorem lt_iInf_iff : a < iInf f ↔ ∃ b, a < b ∧ ∀ i, b ≤ f i :=
  ⟨fun h => ⟨iInf f, h, iInf_le f⟩, fun ⟨_, h, hb⟩ => h.trans_le <| le_iInf hb⟩

Characterization of Strictly Below Infimum: $a < \bigsqcap_i f(i) \leftrightarrow \exists b, a < b \leq f(i) \forall i$

Informal description

For any element $a$ in a complete lattice $\alpha$ and any indexed family of elements $f : \iota \to \alpha$, the inequality $a < \bigsqcap_i f(i)$ holds if and only if there exists an element $b \in \alpha$ such that $a < b$ and $b$ is a lower bound for $f$ (i.e., $b \leq f(i)$ for all $i \in \iota$).

sSup_eq_iSup theorem

{s : Set α} : sSup s = ⨆ a ∈ s, a

Full source

theorem sSup_eq_iSup {s : Set α} : sSup s = ⨆ a ∈ s, a :=
  le_antisymm (sSup_le le_iSup₂) (iSup₂_le fun _ => le_sSup)

Supremum as Indexed Supremum: $\bigvee s = \bigsqcup_{a \in s} a$

Informal description

For any subset $s$ of a complete lattice $\alpha$, the supremum of $s$ is equal to the indexed supremum of all elements in $s$, i.e., $\bigvee s = \bigsqcup_{a \in s} a$.

sInf_eq_iInf theorem

{s : Set α} : sInf s = ⨅ a ∈ s, a

Full source

theorem sInf_eq_iInf {s : Set α} : sInf s = ⨅ a ∈ s, a :=
  @sSup_eq_iSup αᵒᵈ _ _

Infimum as Indexed Infimum: $\bigwedge s = \bigsqcap_{a \in s} a$

Informal description

For any subset $s$ of a complete lattice $\alpha$, the infimum of $s$ is equal to the indexed infimum of all elements in $s$, i.e., $\bigwedge s = \bigsqcap_{a \in s} a$.

sSup_lowerBounds_eq_sInf theorem

(s : Set α) : sSup (lowerBounds s) = sInf s

Full source

lemma sSup_lowerBounds_eq_sInf (s : Set α) : sSup (lowerBounds s) = sInf s :=
  (isLUB_sSup _).unique (isGLB_sInf _).isLUB

Supremum of Lower Bounds Equals Infimum

Informal description

For any subset $s$ of a complete lattice $\alpha$, the supremum of the set of lower bounds of $s$ is equal to the infimum of $s$, i.e., $\bigvee (\text{lowerBounds}(s)) = \bigwedge s$.

sInf_upperBounds_eq_csSup theorem

(s : Set α) : sInf (upperBounds s) = sSup s

Full source

lemma sInf_upperBounds_eq_csSup (s : Set α) : sInf (upperBounds s) = sSup s :=
  (isGLB_sInf _).unique (isLUB_sSup _).isGLB

Infimum of Upper Bounds Equals Supremum: $\bigwedge \text{upperBounds}(s) = \bigvee s$

Informal description

For any subset $s$ of a complete lattice $\alpha$, the infimum of the set of upper bounds of $s$ equals the supremum of $s$, i.e., \[ \bigwedge \{x \in \alpha \mid \forall a \in s, a \leq x\} = \bigvee s. \]

Monotone.le_map_iSup theorem

[CompleteLattice β] {f : α → β} (hf : Monotone f) : ⨆ i, f (s i) ≤ f (iSup s)

Full source

theorem Monotone.le_map_iSup [CompleteLattice β] {f : α → β} (hf : Monotone f) :
    ⨆ i, f (s i) ≤ f (iSup s) :=
  iSup_le fun _ => hf <| le_iSup _ _

Monotonicity Preserves Suprema: $\bigsqcup_i f(s_i) \leq f(\bigsqcup_i s_i)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any indexed family $(s_i)_{i \in \iota}$ in $\alpha$, the supremum of the mapped family $(f(s_i))_{i \in \iota}$ is less than or equal to the image under $f$ of the supremum of $(s_i)_{i \in \iota}$, i.e., \[ \bigsqcup_{i \in \iota} f(s_i) \leq f\left(\bigsqcup_{i \in \iota} s_i\right). \]

Antitone.le_map_iInf theorem

[CompleteLattice β] {f : α → β} (hf : Antitone f) : ⨆ i, f (s i) ≤ f (iInf s)

Full source

theorem Antitone.le_map_iInf [CompleteLattice β] {f : α → β} (hf : Antitone f) :
    ⨆ i, f (s i) ≤ f (iInf s) :=
  hf.dual_left.le_map_iSup

Antitone Function Preserves Infima: $\bigsqcup_i f(s_i) \leq f(\bigsqcap_i s_i)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be an antitone function. For any indexed family $(s_i)_{i \in \iota}$ in $\alpha$, the supremum of the mapped family $(f(s_i))_{i \in \iota}$ is less than or equal to the image under $f$ of the infimum of $(s_i)_{i \in \iota}$, i.e., \[ \bigsqcup_{i \in \iota} f(s_i) \leq f\left(\bigsqcap_{i \in \iota} s_i\right). \]

Monotone.le_map_iSup₂ theorem

 [CompleteLattice β] {f : α → β} (hf : Monotone f) (s : ∀ i, κ i → α) : ⨆ (i) (j), f (s i j) ≤ f (⨆ (i) (j), s i j)

Full source

theorem Monotone.le_map_iSup₂ [CompleteLattice β] {f : α → β} (hf : Monotone f) (s : ∀ i, κ i → α) :
    ⨆ (i) (j), f (s i j) ≤ f (⨆ (i) (j), s i j) :=
  iSup₂_le fun _ _ => hf <| le_iSup₂ _ _

Monotonicity Preserves Double Suprema: $\bigsqcup_{i,j} f(s_{i,j}) \leq f(\bigsqcup_{i,j} s_{i,j})$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any doubly indexed family $(s_{i,j})_{i \in \iota, j \in \kappa_i}$ in $\alpha$, the supremum of the mapped family $(f(s_{i,j}))_{i,j}$ is less than or equal to the image under $f$ of the supremum of $(s_{i,j})_{i,j}$, i.e., \[ \bigsqcup_{i,j} f(s_{i,j}) \leq f\left(\bigsqcup_{i,j} s_{i,j}\right). \]

Antitone.le_map_iInf₂ theorem

 [CompleteLattice β] {f : α → β} (hf : Antitone f) (s : ∀ i, κ i → α) : ⨆ (i) (j), f (s i j) ≤ f (⨅ (i) (j), s i j)

Full source

theorem Antitone.le_map_iInf₂ [CompleteLattice β] {f : α → β} (hf : Antitone f) (s : ∀ i, κ i → α) :
    ⨆ (i) (j), f (s i j) ≤ f (⨅ (i) (j), s i j) :=
  hf.dual_left.le_map_iSup₂ _

Antitone Function Preserves Double Infima: $\bigsqcup_{i,j} f(s_{i,j}) \leq f(\bigsqcap_{i,j} s_{i,j})$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be an antitone function. For any doubly indexed family $(s_{i,j})_{i \in \iota, j \in \kappa_i}$ in $\alpha$, the supremum of the mapped family $(f(s_{i,j}))_{i,j}$ is less than or equal to the image under $f$ of the infimum of $(s_{i,j})_{i,j}$, i.e., \[ \bigsqcup_{i,j} f(s_{i,j}) \leq f\left(\bigsqcap_{i,j} s_{i,j}\right). \]

Monotone.le_map_sSup theorem

[CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) : ⨆ a ∈ s, f a ≤ f (sSup s)

Full source

theorem Monotone.le_map_sSup [CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) :
    ⨆ a ∈ s, f a ≤ f (sSup s) := by rw [sSup_eq_iSup]; exact hf.le_map_iSup₂ _

Monotonicity Preserves Suprema: $\bigsqcup_{a \in s} f(a) \leq f(\bigvee s)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any subset $s \subseteq \alpha$, the supremum of the image of $s$ under $f$ is less than or equal to the image under $f$ of the supremum of $s$, i.e., \[ \bigsqcup_{a \in s} f(a) \leq f\left(\bigvee s\right). \]

Antitone.le_map_sInf theorem

[CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) : ⨆ a ∈ s, f a ≤ f (sInf s)

Full source

theorem Antitone.le_map_sInf [CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) :
    ⨆ a ∈ s, f a ≤ f (sInf s) :=
  hf.dual_left.le_map_sSup

Antitone Function Preserves Infima: $\bigsqcup_{a \in s} f(a) \leq f(\bigsqcap s)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be an antitone function. For any subset $s \subseteq \alpha$, the supremum of the image of $s$ under $f$ is less than or equal to the image under $f$ of the infimum of $s$, i.e., \[ \bigsqcup_{a \in s} f(a) \leq f\left(\bigsqcap s\right). \]

OrderIso.map_iSup theorem

[CompleteLattice β] (f : α ≃o β) (x : ι → α) : f (⨆ i, x i) = ⨆ i, f (x i)

Full source

theorem OrderIso.map_iSup [CompleteLattice β] (f : α ≃o β) (x : ι → α) :
    f (⨆ i, x i) = ⨆ i, f (x i) :=
  eq_of_forall_ge_iff <| f.surjective.forall.2
  fun x => by simp only [f.le_iff_le, iSup_le_iff]

Order Isomorphism Preserves Indexed Suprema: $f(\bigsqcup_i x_i) = \bigsqcup_i f(x_i)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \simeq_o \beta$ be an order isomorphism. For any indexed family of elements $(x_i)_{i \in \iota}$ in $\alpha$, the image under $f$ of their supremum equals the supremum of their images, i.e., \[ f\left(\bigsqcup_{i} x_i\right) = \bigsqcup_{i} f(x_i). \]

OrderIso.map_iInf theorem

[CompleteLattice β] (f : α ≃o β) (x : ι → α) : f (⨅ i, x i) = ⨅ i, f (x i)

Full source

theorem OrderIso.map_iInf [CompleteLattice β] (f : α ≃o β) (x : ι → α) :
    f (⨅ i, x i) = ⨅ i, f (x i) :=
  OrderIso.map_iSup f.dual _

Order Isomorphism Preserves Indexed Infima: $f(\bigsqcap_i x_i) = \bigsqcap_i f(x_i)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \simeq_o \beta$ be an order isomorphism. For any indexed family of elements $(x_i)_{i \in \iota}$ in $\alpha$, the image under $f$ of their infimum equals the infimum of their images, i.e., \[ f\left(\bigsqcap_{i} x_i\right) = \bigsqcap_{i} f(x_i). \]

OrderIso.map_sSup theorem

[CompleteLattice β] (f : α ≃o β) (s : Set α) : f (sSup s) = ⨆ a ∈ s, f a

Full source

theorem OrderIso.map_sSup [CompleteLattice β] (f : α ≃o β) (s : Set α) :
    f (sSup s) = ⨆ a ∈ s, f a := by
  simp only [sSup_eq_iSup, OrderIso.map_iSup]

Order Isomorphism Preserves Suprema: $f(\bigvee s) = \bigsqcup_{a \in s} f(a)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \simeq_o \beta$ be an order isomorphism. For any subset $s \subseteq \alpha$, the image under $f$ of the supremum of $s$ equals the supremum of the images of elements in $s$, i.e., \[ f\left(\bigvee s\right) = \bigsqcup_{a \in s} f(a). \]

OrderIso.map_sInf theorem

[CompleteLattice β] (f : α ≃o β) (s : Set α) : f (sInf s) = ⨅ a ∈ s, f a

Full source

theorem OrderIso.map_sInf [CompleteLattice β] (f : α ≃o β) (s : Set α) :
    f (sInf s) = ⨅ a ∈ s, f a :=
  OrderIso.map_sSup f.dual _

Order Isomorphism Preserves Infima: $f(\bigwedge s) = \bigwedge_{a \in s} f(a)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \simeq_o \beta$ be an order isomorphism. For any subset $s \subseteq \alpha$, the image under $f$ of the infimum of $s$ equals the infimum of the images of elements in $s$, i.e., \[ f\left(\bigwedge s\right) = \bigwedge_{a \in s} f(a). \]

iSup_comp_le theorem

{ι' : Sort*} (f : ι' → α) (g : ι → ι') : ⨆ x, f (g x) ≤ ⨆ y, f y

Full source

theorem iSup_comp_le {ι' : Sort*} (f : ι' → α) (g : ι → ι') : ⨆ x, f (g x) ≤ ⨆ y, f y :=
  iSup_mono' fun _ => ⟨_, le_rfl⟩

Supremum of Composition is Bounded by Supremum of Original Function

Informal description

For any indexed family of elements $f : \iota' \to \alpha$ in a complete lattice $\alpha$ and any function $g : \iota \to \iota'$, the supremum of the composition $f \circ g$ is less than or equal to the supremum of $f$, i.e., \[ \bigsqcup_{x} f(g(x)) \leq \bigsqcup_{y} f(y). \]

le_iInf_comp theorem

{ι' : Sort*} (f : ι' → α) (g : ι → ι') : ⨅ y, f y ≤ ⨅ x, f (g x)

Full source

theorem le_iInf_comp {ι' : Sort*} (f : ι' → α) (g : ι → ι') : ⨅ y, f y ≤ ⨅ x, f (g x) :=
  iInf_mono' fun _ => ⟨_, le_rfl⟩

Infimum Comparison for Composed Functions: $\bigsqcap_y f(y) \leq \bigsqcap_x f(g(x))$

Informal description

For any indexed family of elements $f : \iota' \to \alpha$ in a complete lattice $\alpha$ and any function $g : \iota \to \iota'$, the infimum of $f$ over all indices in $\iota'$ is less than or equal to the infimum of the composition $f \circ g$ over all indices in $\iota$, i.e., \[ \bigsqcap_{y \in \iota'} f(y) \leq \bigsqcap_{x \in \iota} f(g(x)). \]

Monotone.iSup_comp_eq theorem

 [Preorder β] {f : β → α} (hf : Monotone f) {s : ι → β} (hs : ∀ x, ∃ i, x ≤ s i) : ⨆ x, f (s x) = ⨆ y, f y

Full source

theorem Monotone.iSup_comp_eq [Preorder β] {f : β → α} (hf : Monotone f) {s : ι → β}
    (hs : ∀ x, ∃ i, x ≤ s i) : ⨆ x, f (s x) = ⨆ y, f y :=
  le_antisymm (iSup_comp_le _ _) (iSup_mono' fun x => (hs x).imp fun _ hi => hf hi)

Monotone Cofinal Supremum Equality: $\bigsqcup f \circ s = \bigsqcup f$ for cofinal $s$

Informal description

Let $\alpha$ be a complete lattice and $\beta$ a preorder. For a monotone function $f : \beta \to \alpha$ and a family $s : \iota \to \beta$ that is cofinal (i.e., for every $x \in \beta$ there exists $i \in \iota$ such that $x \leq s_i$), the supremum of $f \circ s$ equals the supremum of $f$, i.e., \[ \bigsqcup_{x} f(s_x) = \bigsqcup_{y} f(y). \]

Monotone.iInf_comp_eq theorem

 [Preorder β] {f : β → α} (hf : Monotone f) {s : ι → β} (hs : ∀ x, ∃ i, s i ≤ x) : ⨅ x, f (s x) = ⨅ y, f y

Full source

theorem Monotone.iInf_comp_eq [Preorder β] {f : β → α} (hf : Monotone f) {s : ι → β}
    (hs : ∀ x, ∃ i, s i ≤ x) : ⨅ x, f (s x) = ⨅ y, f y :=
  le_antisymm (iInf_mono' fun x => (hs x).imp fun _ hi => hf hi) (le_iInf_comp _ _)

Monotone Function Infimum Equality: $\bigsqcap_x f(s(x)) = \bigsqcap_y f(y)$ under cofinality condition

Informal description

Let $\alpha$ be a complete lattice and $\beta$ a preorder. For a monotone function $f : \beta \to \alpha$ and a family of elements $s : \iota \to \beta$ such that for every $x \in \beta$ there exists $i \in \iota$ with $s(i) \leq x$, the infimum of $f$ over the range of $s$ equals the infimum of $f$ over all of $\beta$, i.e., \[ \bigsqcap_{x \in \iota} f(s(x)) = \bigsqcap_{y \in \beta} f(y). \]

Antitone.map_iSup_le theorem

[CompleteLattice β] {f : α → β} (hf : Antitone f) : f (iSup s) ≤ ⨅ i, f (s i)

Full source

theorem Antitone.map_iSup_le [CompleteLattice β] {f : α → β} (hf : Antitone f) :
    f (iSup s) ≤ ⨅ i, f (s i) :=
  le_iInf fun _ => hf <| le_iSup _ _

Antitone Function Maps Supremum Below Infimum: $f(\bigsqcup_i s_i) \leq \bigsqcap_i f(s_i)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be an antitone function. For any indexed family $s : \iota \to \alpha$, the value of $f$ at the supremum of $s$ is less than or equal to the infimum of $f$ applied to $s$, i.e., \[ f\left(\bigsqcup_i s_i\right) \leq \bigsqcap_i f(s_i). \]

Monotone.map_iInf_le theorem

[CompleteLattice β] {f : α → β} (hf : Monotone f) : f (iInf s) ≤ ⨅ i, f (s i)

Full source

theorem Monotone.map_iInf_le [CompleteLattice β] {f : α → β} (hf : Monotone f) :
    f (iInf s) ≤ ⨅ i, f (s i) :=
  hf.dual_left.map_iSup_le

Monotone Function Maps Infimum Below Infimum: $f(\bigsqcap_i s_i) \leq \bigsqcap_i f(s_i)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any indexed family $s : \iota \to \alpha$, the value of $f$ at the infimum of $s$ is less than or equal to the infimum of $f$ applied to $s$, i.e., \[ f\left(\bigsqcap_i s_i\right) \leq \bigsqcap_i f(s_i). \]

Antitone.map_iSup₂_le theorem

 [CompleteLattice β] {f : α → β} (hf : Antitone f) (s : ∀ i, κ i → α) : f (⨆ (i) (j), s i j) ≤ ⨅ (i) (j), f (s i j)

Full source

theorem Antitone.map_iSup₂_le [CompleteLattice β] {f : α → β} (hf : Antitone f) (s : ∀ i, κ i → α) :
    f (⨆ (i) (j), s i j) ≤ ⨅ (i) (j), f (s i j) :=
  hf.dual.le_map_iInf₂ _

Antitone Function Maps Double Supremum Below Double Infimum: $f(\bigsqcup_{i,j} s_{i,j}) \leq \bigsqcap_{i,j} f(s_{i,j})$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be an antitone function. For any doubly indexed family $(s_{i,j})_{i \in \iota, j \in \kappa_i}$ in $\alpha$, the value of $f$ at the supremum of $(s_{i,j})_{i,j}$ is less than or equal to the infimum of $(f(s_{i,j}))_{i,j}$, i.e., \[ f\left(\bigsqcup_{i,j} s_{i,j}\right) \leq \bigsqcap_{i,j} f(s_{i,j}). \]

Monotone.map_iInf₂_le theorem

 [CompleteLattice β] {f : α → β} (hf : Monotone f) (s : ∀ i, κ i → α) : f (⨅ (i) (j), s i j) ≤ ⨅ (i) (j), f (s i j)

Full source

theorem Monotone.map_iInf₂_le [CompleteLattice β] {f : α → β} (hf : Monotone f) (s : ∀ i, κ i → α) :
    f (⨅ (i) (j), s i j) ≤ ⨅ (i) (j), f (s i j) :=
  hf.dual.le_map_iSup₂ _

Monotonicity Preserves Double Infima: $f(\bigsqcap_{i,j} s_{i,j}) \leq \bigsqcap_{i,j} f(s_{i,j})$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any doubly indexed family $(s_{i,j})_{i \in \iota, j \in \kappa_i}$ in $\alpha$, the value of $f$ at the infimum of $(s_{i,j})_{i,j}$ is less than or equal to the infimum of $(f(s_{i,j}))_{i,j}$, i.e., \[ f\left(\bigsqcap_{i,j} s_{i,j}\right) \leq \bigsqcap_{i,j} f(s_{i,j}). \]

Antitone.map_sSup_le theorem

[CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) : f (sSup s) ≤ ⨅ a ∈ s, f a

Full source

theorem Antitone.map_sSup_le [CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) :
    f (sSup s) ≤ ⨅ a ∈ s, f a := by
  rw [sSup_eq_iSup]
  exact hf.map_iSup₂_le _

Antitone Function Maps Supremum Below Infimum: $f(\bigvee s) \leq \bigwedge_{a \in s} f(a)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be an antitone function. For any subset $s \subseteq \alpha$, the value of $f$ at the supremum of $s$ is less than or equal to the infimum of $f$ over $s$, i.e., \[ f\left(\bigvee s\right) \leq \bigwedge_{a \in s} f(a). \]

Monotone.map_sInf_le theorem

[CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) : f (sInf s) ≤ ⨅ a ∈ s, f a

Full source

theorem Monotone.map_sInf_le [CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) :
    f (sInf s) ≤ ⨅ a ∈ s, f a :=
  hf.dual_left.map_sSup_le

Monotonicity Preserves Infima: $f(\bigwedge s) \leq \bigwedge_{a \in s} f(a)$

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any subset $s \subseteq \alpha$, the value of $f$ at the infimum of $s$ is less than or equal to the infimum of $f$ over $s$, i.e., \[ f\left(\bigwedge s\right) \leq \bigwedge_{a \in s} f(a). \]

iSup_const_le theorem

: ⨆ _ : ι, a ≤ a

Full source

theorem iSup_const_le : ⨆ _ : ι, a ≤ a :=
  iSup_le fun _ => le_rfl

Supremum of a Constant Family is Bounded by the Constant

Informal description

For any element $a$ in a complete lattice $\alpha$ and any index type $\iota$, the supremum of the constant function $\lambda (i : \iota), a$ is less than or equal to $a$, i.e., $\bigsqcup_{i \in \iota} a \leq a$.

le_iInf_const theorem

: a ≤ ⨅ _ : ι, a

Full source

theorem le_iInf_const : a ≤ ⨅ _ : ι, a :=
  le_iInf fun _ => le_rfl

Element is Below Constant Infimum: $a \leq \bigsqcap_{i} a$

Informal description

For any element $a$ in a complete lattice and any index type $\iota$, the element $a$ is less than or equal to the infimum of the constant function that maps every index to $a$, i.e., $a \leq \bigsqcap_{i \in \iota} a$.

iSup_const theorem

[Nonempty ι] : ⨆ _ : ι, a = a

Full source

theorem iSup_const [Nonempty ι] : ⨆ _ : ι, a = a := by rw [iSup, range_const, sSup_singleton]

Supremum of Constant Function: $\bigsqcup_{i} a = a$

Informal description

For any nonempty index type $\iota$ and any element $a$ in a complete lattice $\alpha$, the supremum of the constant function mapping every index to $a$ is equal to $a$, i.e., $\bigsqcup_{i \in \iota} a = a$.

iInf_const theorem

[Nonempty ι] : ⨅ _ : ι, a = a

Full source

theorem iInf_const [Nonempty ι] : ⨅ _ : ι, a = a :=
  @iSup_const αᵒᵈ _ _ a _

Infimum of Constant Function: $\bigsqcap_{i} a = a$

Informal description

For any nonempty index type $\iota$ and any element $a$ in a complete lattice $\alpha$, the infimum of the constant function mapping every index to $a$ is equal to $a$, i.e., $\bigsqcap_{i \in \iota} a = a$.

iSup_unique theorem

[Unique ι] (f : ι → α) : ⨆ i, f i = f default

Full source

lemma iSup_unique [Unique ι] (f : ι → α) : ⨆ i, f i = f default := by
  simp only [congr_arg f (Unique.eq_default _), iSup_const]

Supremum over Unique Index Type: $\bigsqcup_i f(i) = f(\mathrm{default})$

Informal description

For any complete lattice $\alpha$ and any unique index type $\iota$ (i.e., $\iota$ has exactly one element), the supremum of a function $f \colon \iota \to \alpha$ is equal to the value of $f$ at the default element of $\iota$, i.e., $\bigsqcup_{i \in \iota} f(i) = f(\mathrm{default})$.

iInf_unique theorem

[Unique ι] (f : ι → α) : ⨅ i, f i = f default

Full source

lemma iInf_unique [Unique ι] (f : ι → α) : ⨅ i, f i = f default := by
  simp only [congr_arg f (Unique.eq_default _), iInf_const]

Infimum over Unique Index Type: $\bigsqcap_i f(i) = f(\mathrm{default})$

Informal description

For any complete lattice $\alpha$ and any unique index type $\iota$ (i.e., $\iota$ has exactly one element), the infimum of a function $f \colon \iota \to \alpha$ is equal to the value of $f$ at the default element of $\iota$, i.e., $\bigsqcap_{i \in \iota} f(i) = f(\mathrm{default})$.

iSup_bot theorem

: (⨆ _ : ι, ⊥ : α) = ⊥

Full source

@[simp]
theorem iSup_bot : (⨆ _ : ι, ⊥ : α) = ⊥ :=
  bot_unique iSup_const_le

Supremum of Bottom Elements is Bottom

Informal description

In any complete lattice $\alpha$ with a bottom element $\bot$, the supremum of a constant family of $\bot$ over any index type $\iota$ is equal to $\bot$, i.e., $\bigsqcup_{i \in \iota} \bot = \bot$.

iInf_top theorem

: (⨅ _ : ι, ⊤ : α) = ⊤

Full source

@[simp]
theorem iInf_top : (⨅ _ : ι, ⊤ : α) = ⊤ :=
  top_unique le_iInf_const

Infimum of Constant Top Family Equals Top

Informal description

In any complete lattice $\alpha$, the infimum of a constant family mapping every index to the top element $\top$ is equal to $\top$, i.e., $\bigsqcap_{i \in \iota} \top = \top$.

iSup_eq_bot theorem

: iSup s = ⊥ ↔ ∀ i, s i = ⊥

Full source

@[simp]
theorem iSup_eq_bot : iSupiSup s = ⊥ ↔ ∀ i, s i = ⊥ :=
  sSup_eq_bot.trans forall_mem_range

Characterization of Supremum as Bottom Element: $\bigsqcup_i s_i = \bot \leftrightarrow \forall i, s_i = \bot$

Informal description

For any indexed family of elements $(s_i)_{i \in \iota}$ in a complete lattice $\alpha$, the supremum $\bigsqcup_{i} s_i$ equals the bottom element $\bot$ if and only if $s_i = \bot$ for every index $i$.

iInf_eq_top theorem

: iInf s = ⊤ ↔ ∀ i, s i = ⊤

Full source

@[simp]
theorem iInf_eq_top : iInfiInf s = ⊤ ↔ ∀ i, s i = ⊤ :=
  sInf_eq_top.trans forall_mem_range

Characterization of Infimum as Top: $\bigsqcap_i s_i = \top \leftrightarrow \forall i, s_i = \top$

Informal description

For an indexed family of elements $(s_i)_{i \in \iota}$ in a complete lattice $\alpha$, the infimum $\bigsqcap_i s_i$ equals the top element $\top$ if and only if $s_i = \top$ for every index $i$.

bot_lt_iSup theorem

: ⊥ < ⨆ i, s i ↔ ∃ i, ⊥ < s i

Full source

@[simp] lemma bot_lt_iSup : ⊥⊥ < ⨆ i, s i ↔ ∃ i, ⊥ < s i := by simp [bot_lt_iff_ne_bot]

$\bot < \bigsqcup_i s_i$ iff some $s_i > \bot$

Informal description

In a complete lattice $\alpha$, the supremum $\bigsqcup_i s_i$ is strictly greater than the bottom element $\bot$ if and only if there exists an index $i$ such that $s_i$ is strictly greater than $\bot$.

iInf_lt_top theorem

: ⨅ i, s i < ⊤ ↔ ∃ i, s i < ⊤

Full source

@[simp] lemma iInf_lt_top : ⨅ i, s i⨅ i, s i < ⊤ ↔ ∃ i, s i < ⊤ := by simp [lt_top_iff_ne_top]

Infimum is Less Than Top if and only if Some Element is Less Than Top

Informal description

For an indexed family of elements $(s_i)_{i \in \iota}$ in a complete lattice $\alpha$, the infimum $\bigsqcap_i s_i$ is strictly less than the top element $\top$ if and only if there exists some index $i$ such that $s_i < \top$.

iSup₂_eq_bot theorem

{f : ∀ i, κ i → α} : ⨆ (i) (j), f i j = ⊥ ↔ ∀ i j, f i j = ⊥

Full source

theorem iSup₂_eq_bot {f : ∀ i, κ i → α} : ⨆ (i) (j), f i j⨆ (i) (j), f i j = ⊥ ↔ ∀ i j, f i j = ⊥ := by
  simp

Supremum of Family Equals Bottom Element if and only if All Elements are Bottom

Informal description

For a family of elements $f_{i,j}$ in a complete lattice $\alpha$, the supremum $\bigsqcup_{i,j} f_{i,j}$ equals the bottom element $\bot$ if and only if $f_{i,j} = \bot$ for all $i$ and $j$.

iInf₂_eq_top theorem

{f : ∀ i, κ i → α} : ⨅ (i) (j), f i j = ⊤ ↔ ∀ i j, f i j = ⊤

Full source

theorem iInf₂_eq_top {f : ∀ i, κ i → α} : ⨅ (i) (j), f i j⨅ (i) (j), f i j = ⊤ ↔ ∀ i j, f i j = ⊤ := by
  simp

Double Infimum Equals Top iff All Elements are Top

Informal description

For a family of elements $f_{i,j}$ in a complete lattice $\alpha$, the double infimum $\bigsqcap_{i,j} f_{i,j}$ equals the top element $\top$ if and only if $f_{i,j} = \top$ for all indices $i$ and $j$.

iSup_pos theorem

{p : Prop} {f : p → α} (hp : p) : ⨆ h : p, f h = f hp

Full source

@[simp]
theorem iSup_pos {p : Prop} {f : p → α} (hp : p) : ⨆ h : p, f h = f hp :=
  le_antisymm (iSup_le fun _ => le_rfl) (le_iSup _ _)

Supremum over True Proposition Equals Function Value

Informal description

For any proposition $p$ and any function $f : p \to \alpha$ in a complete lattice $\alpha$, if $p$ holds (with proof $hp$), then the supremum of $f$ over all proofs of $p$ equals $f(hp)$. That is, $\bigsqcup_{h : p} f(h) = f(hp)$.

iInf_pos theorem

{p : Prop} {f : p → α} (hp : p) : ⨅ h : p, f h = f hp

Full source

@[simp]
theorem iInf_pos {p : Prop} {f : p → α} (hp : p) : ⨅ h : p, f h = f hp :=
  le_antisymm (iInf_le _ _) (le_iInf fun _ => le_rfl)

Infimum over a true proposition equals its value

Informal description

For any proposition $p$ and any function $f : p \to \alpha$ into a complete lattice $\alpha$, if $p$ holds (with proof $hp$), then the infimum $\bigsqcap_{h : p} f(h)$ equals $f(hp)$.

iSup_neg theorem

{p : Prop} {f : p → α} (hp : ¬p) : ⨆ h : p, f h = ⊥

Full source

@[simp]
theorem iSup_neg {p : Prop} {f : p → α} (hp : ¬p) : ⨆ h : p, f h = ⊥ :=
  le_antisymm (iSup_le fun h => (hp h).elim) bot_le

Supremum over False Proposition is Bottom Element

Informal description

For any proposition $p$ and any function $f : p \to \alpha$ from $p$ to a complete lattice $\alpha$, if $p$ is false ($\neg p$ holds), then the supremum of $f$ over all proofs of $p$ is equal to the bottom element $\bot$ of $\alpha$. That is, $\bigsqcup_{h : p} f(h) = \bot$.

iInf_neg theorem

{p : Prop} {f : p → α} (hp : ¬p) : ⨅ h : p, f h = ⊤

Full source

@[simp]
theorem iInf_neg {p : Prop} {f : p → α} (hp : ¬p) : ⨅ h : p, f h = ⊤ :=
  le_antisymm le_top <| le_iInf fun h => (hp h).elim

Infimum over False Proposition is Top Element

Informal description

For any proposition $p$ and any function $f : p \to \alpha$ from $p$ to a complete lattice $\alpha$, if $p$ is false ($\neg p$), then the infimum of $f$ over all $h : p$ is equal to the top element $\top$ of $\alpha$, i.e., $\bigsqcap_{h : p} f(h) = \top$.

iSup_eq_of_forall_le_of_forall_lt_exists_gt theorem

{f : ι → α} (h₁ : ∀ i, f i ≤ b) (h₂ : ∀ w, w < b → ∃ i, w < f i) : ⨆ i : ι, f i = b

Full source

/-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
See `ciSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in conditionally complete
lattices. -/
theorem iSup_eq_of_forall_le_of_forall_lt_exists_gt {f : ι → α} (h₁ : ∀ i, f i ≤ b)
    (h₂ : ∀ w, w < b → ∃ i, w < f i) : ⨆ i : ι, f i = b :=
  sSup_eq_of_forall_le_of_forall_lt_exists_gt (forall_mem_range.mpr h₁) fun w hw =>
    exists_range_iff.mpr <| h₂ w hw

Characterization of indexed supremum via upper bounds and strict lower bounds

Informal description

Let $f : \iota \to \alpha$ be a function from an index set $\iota$ to a complete lattice $\alpha$, and let $b \in \alpha$. If: 1. $f(i) \leq b$ for all $i \in \iota$, and 2. for every $w < b$, there exists $i \in \iota$ such that $w < f(i)$, then the supremum of the range of $f$ is equal to $b$, i.e., $\bigsqcup_{i \in \iota} f(i) = b$.

iInf_eq_of_forall_ge_of_forall_gt_exists_lt theorem

: (∀ i, b ≤ f i) → (∀ w, b < w → ∃ i, f i < w) → ⨅ i, f i = b

Full source

/-- 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 iInf_eq_of_forall_ge_of_forall_gt_exists_lt :
    (∀ i, b ≤ f i) → (∀ w, b < w → ∃ i, f i < w) → ⨅ i, f i = b :=
  @iSup_eq_of_forall_le_of_forall_lt_exists_gt αᵒᵈ _ _ _ _

Characterization of Indexed Infimum via Lower Bounds and Strict Upper Bounds

Informal description

Let $\alpha$ be a complete lattice, $f : \iota \to \alpha$ an indexed family of elements, and $b \in \alpha$. If: 1. $b \leq f(i)$ for all $i \in \iota$, and 2. for every $w > b$, there exists $i \in \iota$ such that $f(i) < w$, then the infimum of the range of $f$ is equal to $b$, i.e., $\bigsqcap_{i \in \iota} f(i) = b$.

iSup_eq_dif theorem

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

Full source

theorem iSup_eq_dif {p : Prop} [Decidable p] (a : p → α) :
    ⨆ h : p, a h = if h : p then a h else ⊥ := by by_cases h : p <;> simp [h]

Supremum over Decidable Proposition as Conditional Expression

Informal description

Let $p$ be a decidable proposition and $a : p \to \alpha$ a function from proofs of $p$ to a complete lattice $\alpha$. Then the supremum of $a$ over all proofs of $p$ equals $a(h)$ if $p$ holds (with proof $h$), and equals the bottom element $\bot$ otherwise. That is, \[ \bigsqcup_{h : p} a(h) = \begin{cases} a(h) & \text{if } p \text{ holds (with proof } h\text{)} \\ \bot & \text{otherwise.} \end{cases} \]

iSup_eq_if theorem

{p : Prop} [Decidable p] (a : α) : ⨆ _ : p, a = if p then a else ⊥

Full source

theorem iSup_eq_if {p : Prop} [Decidable p] (a : α) : ⨆ _ : p, a = if p then a else ⊥ :=
  iSup_eq_dif fun _ => a

Supremum of Constant Function over Proposition as Conditional Expression

Informal description

Let $p$ be a decidable proposition and $a$ an element of a complete lattice $\alpha$. Then the supremum of the constant function equal to $a$ over all proofs of $p$ is equal to $a$ if $p$ holds, and is equal to the bottom element $\bot$ otherwise. That is, \[ \bigsqcup_{\_ : p} a = \begin{cases} a & \text{if } p \text{ holds} \\ \bot & \text{otherwise.} \end{cases} \]

iInf_eq_dif theorem

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

Full source

theorem iInf_eq_dif {p : Prop} [Decidable p] (a : p → α) :
    ⨅ h : p, a h = if h : p then a h else ⊤ :=
  @iSup_eq_dif αᵒᵈ _ _ _ _

Infimum over Decidable Proposition as Conditional Expression

Informal description

Let $p$ be a decidable proposition and $a : p \to \alpha$ a function from proofs of $p$ to a complete lattice $\alpha$. Then the infimum of $a$ over all proofs of $p$ equals $a(h)$ if $p$ holds (with proof $h$), and equals the top element $\top$ otherwise. That is, \[ \bigsqcap_{h : p} a(h) = \begin{cases} a(h) & \text{if } p \text{ holds (with proof } h\text{)} \\ \top & \text{otherwise.} \end{cases} \]

iInf_eq_if theorem

{p : Prop} [Decidable p] (a : α) : ⨅ _ : p, a = if p then a else ⊤

Full source

theorem iInf_eq_if {p : Prop} [Decidable p] (a : α) : ⨅ _ : p, a = if p then a else ⊤ :=
  iInf_eq_dif fun _ => a

Infimum of Constant Function over Proposition as Conditional Expression

Informal description

Let $p$ be a decidable proposition and $a$ an element of a complete lattice $\alpha$. Then the infimum of the constant function equal to $a$ over all proofs of $p$ is equal to $a$ if $p$ holds, and is equal to the top element $\top$ otherwise. That is, \[ \bigsqcap_{\_ : p} a = \begin{cases} a & \text{if } p \text{ holds} \\ \top & \text{otherwise.} \end{cases} \]

iSup_comm theorem

{f : ι → ι' → α} : ⨆ (i) (j), f i j = ⨆ (j) (i), f i j

Full source

theorem iSup_comm {f : ι → ι' → α} : ⨆ (i) (j), f i j = ⨆ (j) (i), f i j :=
  le_antisymm (iSup_le fun i => iSup_mono fun j => le_iSup (fun i => f i j) i)
    (iSup_le fun _ => iSup_mono fun _ => le_iSup _ _)

Commutativity of Double Suprema: $\bigsqcup_i \bigsqcup_j f(i,j) = \bigsqcup_j \bigsqcup_i f(i,j)$

Informal description

For any doubly indexed family of elements $f : \iota \times \iota' \to \alpha$ in a complete lattice $\alpha$, the supremum over the first index followed by the second index is equal to the supremum over the second index followed by the first index, i.e., \[ \bigsqcup_{i \in \iota} \bigsqcup_{j \in \iota'} f(i, j) = \bigsqcup_{j \in \iota'} \bigsqcup_{i \in \iota} f(i, j). \]

iInf_comm theorem

{f : ι → ι' → α} : ⨅ (i) (j), f i j = ⨅ (j) (i), f i j

Full source

theorem iInf_comm {f : ι → ι' → α} : ⨅ (i) (j), f i j = ⨅ (j) (i), f i j :=
  @iSup_comm αᵒᵈ _ _ _ _

Commutativity of Double Infima: $\bigsqcap_i \bigsqcap_j f(i,j) = \bigsqcap_j \bigsqcap_i f(i,j)$

Informal description

For any doubly indexed family of elements $f : \iota \times \iota' \to \alpha$ in a complete lattice $\alpha$, the infimum over the first index followed by the second index is equal to the infimum over the second index followed by the first index, i.e., \[ \bigsqcap_{i \in \iota} \bigsqcap_{j \in \iota'} f(i, j) = \bigsqcap_{j \in \iota'} \bigsqcap_{i \in \iota} f(i, j). \]

iSup₂_comm theorem

 {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} (f : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → α) :
  ⨆ (i₁) (j₁) (i₂) (j₂), f i₁ j₁ i₂ j₂ = ⨆ (i₂) (j₂) (i₁) (j₁), f i₁ j₁ i₂ j₂

Full source

theorem iSup₂_comm {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*}
    (f : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → α) :
    ⨆ (i₁) (j₁) (i₂) (j₂), f i₁ j₁ i₂ j₂ = ⨆ (i₂) (j₂) (i₁) (j₁), f i₁ j₁ i₂ j₂ := by
  simp only [@iSup_comm _ (κ₁ _), @iSup_comm _ ι₁]

Commutativity of Quadruple Suprema: $\bigsqcup_{i_1,j_1,i_2,j_2} f(i_1,j_1,i_2,j_2) = \bigsqcup_{i_2,j_2,i_1,j_1} f(i_1,j_1,i_2,j_2)$

Informal description

For any doubly indexed family of elements $f : \Pi (i_1 : \iota_1) (j_1 : \kappa_1(i_1)) (i_2 : \iota_2) (j_2 : \kappa_2(i_2)) \to \alpha$ in a complete lattice $\alpha$, the iterated supremum over the first two indices followed by the last two indices is equal to the iterated supremum over the last two indices followed by the first two indices, i.e., \[ \bigsqcup_{i_1} \bigsqcup_{j_1} \bigsqcup_{i_2} \bigsqcup_{j_2} f(i_1, j_1, i_2, j_2) = \bigsqcup_{i_2} \bigsqcup_{j_2} \bigsqcup_{i_1} \bigsqcup_{j_1} f(i_1, j_1, i_2, j_2). \]

iInf₂_comm theorem

 {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} (f : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → α) :
  ⨅ (i₁) (j₁) (i₂) (j₂), f i₁ j₁ i₂ j₂ = ⨅ (i₂) (j₂) (i₁) (j₁), f i₁ j₁ i₂ j₂

Full source

theorem iInf₂_comm {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*}
    (f : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → α) :
    ⨅ (i₁) (j₁) (i₂) (j₂), f i₁ j₁ i₂ j₂ = ⨅ (i₂) (j₂) (i₁) (j₁), f i₁ j₁ i₂ j₂ := by
  simp only [@iInf_comm _ (κ₁ _), @iInf_comm _ ι₁]

Commutativity of Quadruple Infima: $\bigsqcap_{i_1,j_1,i_2,j_2} f(i_1,j_1,i_2,j_2) = \bigsqcap_{i_2,j_2,i_1,j_1} f(i_1,j_1,i_2,j_2)$

Informal description

For any doubly indexed family of elements $f : \Pi (i_1 : \iota_1) (j_1 : \kappa_1(i_1)) (i_2 : \iota_2) (j_2 : \kappa_2(i_2)) \to \alpha$ in a complete lattice $\alpha$, the iterated infimum over the first two indices followed by the last two indices is equal to the iterated infimum over the last two indices followed by the first two indices, i.e., \[ \bigsqcap_{i_1} \bigsqcap_{j_1} \bigsqcap_{i_2} \bigsqcap_{j_2} f(i_1, j_1, i_2, j_2) = \bigsqcap_{i_2} \bigsqcap_{j_2} \bigsqcap_{i_1} \bigsqcap_{j_1} f(i_1, j_1, i_2, j_2). \]

iSup_iSup_eq_left theorem

{b : β} {f : ∀ x : β, x = b → α} : ⨆ x, ⨆ h : x = b, f x h = f b rfl

Full source

@[simp]
theorem iSup_iSup_eq_left {b : β} {f : ∀ x : β, x = b → α} : ⨆ x, ⨆ h : x = b, f x h = f b rfl :=
  (@le_iSup₂ _ _ _ _ f b rfl).antisymm'
    (iSup_le fun c =>
      iSup_le <| by
        rintro rfl
        rfl)

Double Supremum Equality for Diagonal Case: $\bigsqcup_{x} \bigsqcup_{h : x = b} f(x, h) = f(b, \text{refl})$

Informal description

For any type $\beta$, element $b \in \beta$, and function $f$ defined for all $x \in \beta$ with $x = b$, the double supremum $\bigsqcup_{x \in \beta} \bigsqcup_{h : x = b} f(x, h)$ equals $f(b, \text{refl})$, where $\text{refl}$ is the reflexivity proof that $b = b$.

iInf_iInf_eq_left theorem

{b : β} {f : ∀ x : β, x = b → α} : ⨅ x, ⨅ h : x = b, f x h = f b rfl

Full source

@[simp]
theorem iInf_iInf_eq_left {b : β} {f : ∀ x : β, x = b → α} : ⨅ x, ⨅ h : x = b, f x h = f b rfl :=
  @iSup_iSup_eq_left αᵒᵈ _ _ _ _

Double Infimum Equality for Diagonal Case: $\bigsqcap_{x} \bigsqcap_{h : x = b} f(x, h) = f(b, \text{refl})$

Informal description

For any type $\beta$, element $b \in \beta$, and function $f$ defined for all $x \in \beta$ with $x = b$, the double infimum $\bigsqcap_{x \in \beta} \bigsqcap_{h : x = b} f(x, h)$ equals $f(b, \text{refl})$, where $\text{refl}$ is the reflexivity proof that $b = b$.

iSup_iSup_eq_right theorem

{b : β} {f : ∀ x : β, b = x → α} : ⨆ x, ⨆ h : b = x, f x h = f b rfl

Full source

@[simp]
theorem iSup_iSup_eq_right {b : β} {f : ∀ x : β, b = x → α} : ⨆ x, ⨆ h : b = x, f x h = f b rfl :=
  (le_iSup₂ b rfl).antisymm'
    (iSup₂_le fun c => by
      rintro rfl
      rfl)

Double Supremum Equality for Right-Equal Indexed Family: $\bigsqcup_{x} \bigsqcup_{h : b = x} f(x, h) = f(b, \text{rfl})$

Informal description

For any element $b$ of type $\beta$ and any family of elements $f : \forall x : \beta, b = x \to \alpha$ indexed by $\beta$ and a proof that $b = x$, the double supremum $\bigsqcup_{x} \bigsqcup_{h : b = x} f(x, h)$ is equal to $f(b, \text{rfl})$, where $\text{rfl}$ is the reflexivity proof that $b = b$.

iInf_iInf_eq_right theorem

{b : β} {f : ∀ x : β, b = x → α} : ⨅ x, ⨅ h : b = x, f x h = f b rfl

Full source

@[simp]
theorem iInf_iInf_eq_right {b : β} {f : ∀ x : β, b = x → α} : ⨅ x, ⨅ h : b = x, f x h = f b rfl :=
  @iSup_iSup_eq_right αᵒᵈ _ _ _ _

Double Infimum Equality for Right-Equal Indexed Family: $\bigsqcap_{x} \bigsqcap_{h : b = x} f(x, h) = f(b, \text{rfl})$

Informal description

For any element $b$ of type $\beta$ and any family of elements $f : \forall x : \beta, b = x \to \alpha$ indexed by $\beta$ and a proof that $b = x$, the double infimum $\bigsqcap_{x} \bigsqcap_{h : b = x} f(x, h)$ is equal to $f(b, \text{rfl})$, where $\text{rfl}$ is the reflexivity proof that $b = b$.

iSup_subtype theorem

{p : ι → Prop} {f : Subtype p → α} : iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩

Full source

theorem iSup_subtype {p : ι → Prop} {f : Subtype p → α} : iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ :=
  le_antisymm (iSup_le fun ⟨i, h⟩ => @le_iSup₂ _ _ p _ (fun i h => f ⟨i, h⟩) i h)
    (iSup₂_le fun _ _ => le_iSup _ _)

Supremum over Subtype Equals Double Supremum

Informal description

For any predicate $p$ on an index type $\iota$ and any function $f$ defined on the subtype $\{i \in \iota \mid p(i)\}$, the supremum of $f$ over the subtype is equal to the double supremum $\bigsqcup_{i \in \iota} \bigsqcup_{h : p(i)} f(\langle i, h \rangle)$.

iInf_subtype theorem

: ∀ {p : ι → Prop} {f : Subtype p → α}, iInf f = ⨅ (i) (h : p i), f ⟨i, h⟩

Full source

theorem iInf_subtype : ∀ {p : ι → Prop} {f : Subtype p → α}, iInf f = ⨅ (i) (h : p i), f ⟨i, h⟩ :=
  @iSup_subtype αᵒᵈ _ _

Infimum over Subtype Equals Double Infimum

Informal description

For any predicate $p$ on an index type $\iota$ and any function $f$ defined on the subtype $\{i \in \iota \mid p(i)\}$, the infimum of $f$ over the subtype is equal to the double infimum $\bigsqcap_{i \in \iota} \bigsqcap_{h : p(i)} f(\langle i, h \rangle)$.

iSup_subtype' theorem

{p : ι → Prop} {f : ∀ i, p i → α} : ⨆ (i) (h), f i h = ⨆ x : Subtype p, f x x.property

Full source

theorem iSup_subtype' {p : ι → Prop} {f : ∀ i, p i → α} :
    ⨆ (i) (h), f i h = ⨆ x : Subtype p, f x x.property :=
  (@iSup_subtype _ _ _ p fun x => f x.val x.property).symm

Double Supremum Equals Supremum over Subtype

Informal description

For any predicate $p$ on an index type $\iota$ and any function $f$ defined for all $i \in \iota$ satisfying $p(i)$, the double supremum $\bigsqcup_{i \in \iota} \bigsqcup_{h : p(i)} f(i, h)$ is equal to the supremum of $f$ over the subtype $\{x \in \iota \mid p(x)\}$, where each element $x$ of the subtype is mapped to $f(x, \text{proof that } p(x))$.

iInf_subtype' theorem

{p : ι → Prop} {f : ∀ i, p i → α} : ⨅ (i) (h : p i), f i h = ⨅ x : Subtype p, f x x.property

Full source

theorem iInf_subtype' {p : ι → Prop} {f : ∀ i, p i → α} :
    ⨅ (i) (h : p i), f i h = ⨅ x : Subtype p, f x x.property :=
  (@iInf_subtype _ _ _ p fun x => f x.val x.property).symm

Double Infimum Equals Infimum over Subtype

Informal description

For any predicate $p$ on an index type $\iota$ and any function $f$ defined for all $i \in \iota$ satisfying $p(i)$, the double infimum $\bigsqcap_{i \in \iota} \bigsqcap_{h : p(i)} f(i, h)$ is equal to the infimum of $f$ over the subtype $\{x \in \iota \mid p(x)\}$, where each element $x$ of the subtype is mapped to $f(x, \text{proof that } p(x))$.

iSup_subtype'' theorem

{ι} (s : Set ι) (f : ι → α) : ⨆ i : s, f i = ⨆ (t : ι) (_ : t ∈ s), f t

Full source

theorem iSup_subtype'' {ι} (s : Set ι) (f : ι → α) : ⨆ i : s, f i = ⨆ (t : ι) (_ : t ∈ s), f t :=
  iSup_subtype

Supremum over Set Equals Bounded Supremum

Informal description

For any set $s$ of elements of type $\iota$ and any function $f : \iota \to \alpha$, the supremum of $f$ over the elements of $s$ is equal to the supremum of $f(t)$ for all $t \in \iota$ such that $t \in s$. In other words: \[ \bigsqcup_{i \in s} f(i) = \bigsqcup_{t \in \iota,\ t \in s} f(t) \]

iInf_subtype'' theorem

{ι} (s : Set ι) (f : ι → α) : ⨅ i : s, f i = ⨅ (t : ι) (_ : t ∈ s), f t

Full source

theorem iInf_subtype'' {ι} (s : Set ι) (f : ι → α) : ⨅ i : s, f i = ⨅ (t : ι) (_ : t ∈ s), f t :=
  iInf_subtype

Infimum over Set Equals Bounded Infimum

Informal description

For any set $s$ of elements of type $\iota$ and any function $f : \iota \to \alpha$, the infimum of $f$ over the elements of $s$ is equal to the infimum of $f(t)$ for all $t \in \iota$ such that $t \in s$. In other words: \[ \bigsqcap_{i \in s} f(i) = \bigsqcap_{t \in \iota,\ t \in s} f(t) \]

biSup_const theorem

{a : α} {s : Set β} (hs : s.Nonempty) : ⨆ i ∈ s, a = a

Full source

theorem biSup_const {a : α} {s : Set β} (hs : s.Nonempty) : ⨆ i ∈ s, a = a := by
  haveI : Nonempty s := Set.nonempty_coe_sort.mpr hs
  rw [← iSup_subtype'', iSup_const]

Bounded Supremum of Constant Function Equals Constant

Informal description

For any element $a$ in a complete lattice $\alpha$ and any nonempty set $s$ of elements of type $\beta$, the bounded supremum of the constant function mapping every $i \in s$ to $a$ is equal to $a$, i.e., \[ \bigsqcup_{i \in s} a = a. \]

biInf_const theorem

{a : α} {s : Set β} (hs : s.Nonempty) : ⨅ i ∈ s, a = a

Full source

theorem biInf_const {a : α} {s : Set β} (hs : s.Nonempty) : ⨅ i ∈ s, a = a :=
  biSup_const (α := αᵒᵈ) hs

Bounded Infimum of Constant Function Equals Constant

Informal description

For any element $a$ in a complete lattice $\alpha$ and any nonempty set $s$ of elements of type $\beta$, the bounded infimum of the constant function mapping every $i \in s$ to $a$ is equal to $a$, i.e., \[ \bigsqcap_{i \in s} a = a. \]

iSup_sup_eq theorem

: ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x

Full source

theorem iSup_sup_eq : ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x :=
  le_antisymm (iSup_le fun _ => sup_le_sup (le_iSup _ _) <| le_iSup _ _)
    (sup_le (iSup_mono fun _ => le_sup_left) <| iSup_mono fun _ => le_sup_right)

Supremum of Pairwise Suprema Equals Supremum of Suprema

Informal description

For any indexed families of elements $(f_x)_{x \in \iota}$ and $(g_x)_{x \in \iota}$ in a complete lattice $\alpha$, the supremum of the pairwise suprema equals the supremum of the suprema, i.e., \[ \bigsqcup_{x} (f_x \sqcup g_x) = \left(\bigsqcup_{x} f_x\right) \sqcup \left(\bigsqcup_{x} g_x\right). \]

iInf_inf_eq theorem

: ⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ ⨅ x, g x

Full source

theorem iInf_inf_eq : ⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ ⨅ x, g x :=
  @iSup_sup_eq αᵒᵈ _ _ _ _

Infimum of Pairwise Infima Equals Infimum of Infima

Informal description

For any indexed families of elements $(f_x)_{x \in \iota}$ and $(g_x)_{x \in \iota}$ in a complete lattice $\alpha$, the infimum of the pairwise infima equals the infimum of the infima, i.e., \[ \bigsqcap_{x} (f_x \sqcap g_x) = \left(\bigsqcap_{x} f_x\right) \sqcap \left(\bigsqcap_{x} g_x\right). \]

Equiv.biSup_comp theorem

{ι ι' : Type*} {g : ι' → α} (e : ι ≃ ι') (s : Set ι') : ⨆ i ∈ e.symm '' s, g (e i) = ⨆ i ∈ s, g i

Full source

lemma Equiv.biSup_comp {ι ι' : Type*} {g : ι' → α} (e : ι ≃ ι') (s : Set ι') :
    ⨆ i ∈ e.symm '' s, g (e i) = ⨆ i ∈ s, g i := by
  simpa only [iSup_subtype'] using (image e.symm s).symm.iSup_comp (g := g ∘ (↑))

Bounded Supremum Preservation under Equivalence: $\bigsqcup_{i \in e^{-1}(s)} g(e(i)) = \bigsqcup_{i \in s} g(i)$

Informal description

Let $\alpha$ be a complete lattice, $\iota$ and $\iota'$ be types, $g : \iota' \to \alpha$ be a function, and $e : \iota \simeq \iota'$ be an equivalence between $\iota$ and $\iota'$. For any subset $s \subseteq \iota'$, the bounded supremum of $g \circ e$ over the preimage $e^{-1}(s)$ equals the bounded supremum of $g$ over $s$, i.e., \[ \bigsqcup_{i \in e^{-1}(s)} g(e(i)) = \bigsqcup_{i \in s} g(i). \]

Equiv.biInf_comp theorem

{ι ι' : Type*} {g : ι' → α} (e : ι ≃ ι') (s : Set ι') : ⨅ i ∈ e.symm '' s, g (e i) = ⨅ i ∈ s, g i

Full source

lemma Equiv.biInf_comp {ι ι' : Type*} {g : ι' → α} (e : ι ≃ ι') (s : Set ι') :
    ⨅ i ∈ e.symm '' s, g (e i) = ⨅ i ∈ s, g i :=
  e.biSup_comp s (α := αᵒᵈ)

Bounded Infimum Preservation under Equivalence: $\bigsqcap_{i \in e^{-1}(s)} g(e(i)) = \bigsqcap_{i \in s} g(i)$

Informal description

Let $\alpha$ be a complete lattice, $\iota$ and $\iota'$ be types, $g : \iota' \to \alpha$ be a function, and $e : \iota \simeq \iota'$ be an equivalence between $\iota$ and $\iota'$. For any subset $s \subseteq \iota'$, the bounded infimum of $g \circ e$ over the preimage $e^{-1}(s)$ equals the bounded infimum of $g$ over $s$, i.e., \[ \bigsqcap_{i \in e^{-1}(s)} g(e(i)) = \bigsqcap_{i \in s} g(i). \]

biInf_le theorem

{ι : Type*} {s : Set ι} (f : ι → α) {i : ι} (hi : i ∈ s) : ⨅ i ∈ s, f i ≤ f i

Full source

lemma biInf_le {ι : Type*} {s : Set ι} (f : ι → α) {i : ι} (hi : i ∈ s) : ⨅ i ∈ s, f i ≤ f i :=
  iInf₂_le i hi

Infimum over a Set is a Lower Bound: $\bigsqcap_{i \in s} f(i) \leq f(i)$

Informal description

For any set $s$ of indices of type $\iota$ and any function $f : \iota \to \alpha$ where $\alpha$ is a complete lattice, if $i \in s$, then the infimum of $f$ over $s$ is less than or equal to $f(i)$, i.e., $\bigsqcap_{i \in s} f(i) \leq f(i)$.

le_biSup theorem

{ι : Type*} {s : Set ι} (f : ι → α) {i : ι} (hi : i ∈ s) : f i ≤ ⨆ i ∈ s, f i

Full source

lemma le_biSup {ι : Type*} {s : Set ι} (f : ι → α) {i : ι} (hi : i ∈ s) : f i ≤ ⨆ i ∈ s, f i :=
  biInf_le (α := αᵒᵈ) f hi

Function Value is Bounded by Supremum over Set: $f(i) \leq \bigsqcup_{i \in s} f(i)$

Informal description

For any set $s$ of indices of type $\iota$ and any function $f : \iota \to \alpha$ where $\alpha$ is a complete lattice, if $i \in s$, then $f(i)$ is less than or equal to the supremum of $f$ over $s$, i.e., $f(i) \leq \bigsqcup_{i \in s} f(i)$.

biInf_le_biSup theorem

{ι : Type*} {s : Set ι} (hs : s.Nonempty) {f : ι → α} : ⨅ i ∈ s, f i ≤ ⨆ i ∈ s, f i

Full source

lemma biInf_le_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty) {f : ι → α} :
    ⨅ i ∈ s, f i ≤ ⨆ i ∈ s, f i :=
  (biInf_le _ hs.choose_spec).trans <| le_biSup _ hs.choose_spec

Infimum over Nonempty Set is Less Than or Equal to Supremum: $\bigsqcap_{i \in s} f(i) \leq \bigsqcup_{i \in s} f(i)$

Informal description

For any nonempty set $s$ of indices of type $\iota$ and any function $f : \iota \to \alpha$ where $\alpha$ is a complete lattice, the infimum of $f$ over $s$ is less than or equal to the supremum of $f$ over $s$, i.e., $\bigsqcap_{i \in s} f(i) \leq \bigsqcup_{i \in s} f(i)$.

iSup_sup theorem

[Nonempty ι] {f : ι → α} {a : α} : (⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a

Full source

theorem iSup_sup [Nonempty ι] {f : ι → α} {a : α} : (⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a := by
  rw [iSup_sup_eq, iSup_const]

Supremum Joins with Element Equals Supremum of Joins: $(\bigsqcup_x f_x) \sqcup a = \bigsqcup_x (f_x \sqcup a)$

Informal description

For any nonempty index type $\iota$ and any function $f : \iota \to \alpha$ where $\alpha$ is a complete lattice, and for any element $a \in \alpha$, the supremum of $f$ joined with $a$ equals the supremum of the functions $f_x \sqcup a$, i.e., \[ \left(\bigsqcup_{x} f_x\right) \sqcup a = \bigsqcup_{x} (f_x \sqcup a). \]

iInf_inf theorem

[Nonempty ι] {f : ι → α} {a : α} : (⨅ x, f x) ⊓ a = ⨅ x, f x ⊓ a

Full source

theorem iInf_inf [Nonempty ι] {f : ι → α} {a : α} : (⨅ x, f x) ⊓ a = ⨅ x, f x ⊓ a := by
  rw [iInf_inf_eq, iInf_const]

Infimum Distributes Over Meet: $(\bigsqcap_x f_x) \sqcap a = \bigsqcap_x (f_x \sqcap a)$

Informal description

For any nonempty index type $\iota$, any function $f : \iota \to \alpha$ where $\alpha$ is a complete lattice, and any element $a \in \alpha$, the infimum of $f$ meets with $a$ equals the infimum of the functions $f_x \sqcap a$, i.e., \[ \left(\bigsqcap_{x} f_x\right) \sqcap a = \bigsqcap_{x} (f_x \sqcap a). \]

sup_iSup theorem

[Nonempty ι] {f : ι → α} {a : α} : (a ⊔ ⨆ x, f x) = ⨆ x, a ⊔ f x

Full source

theorem sup_iSup [Nonempty ι] {f : ι → α} {a : α} : (a ⊔ ⨆ x, f x) = ⨆ x, a ⊔ f x := by
  rw [iSup_sup_eq, iSup_const]

Supremum Distributes Over Join: $a \sqcup \bigsqcup_x f_x = \bigsqcup_x (a \sqcup f_x)$

Informal description

For any nonempty index type $\iota$, any element $a$ in a complete lattice $\alpha$, and any indexed family of elements $(f_x)_{x \in \iota}$ in $\alpha$, the supremum of $a$ with the supremum of the family equals the supremum of the family obtained by taking the supremum of $a$ with each element of the family, i.e., \[ a \sqcup \left(\bigsqcup_{x} f_x\right) = \bigsqcup_{x} (a \sqcup f_x). \]

inf_iInf theorem

[Nonempty ι] {f : ι → α} {a : α} : (a ⊓ ⨅ x, f x) = ⨅ x, a ⊓ f x

Full source

theorem inf_iInf [Nonempty ι] {f : ι → α} {a : α} : (a ⊓ ⨅ x, f x) = ⨅ x, a ⊓ f x := by
  rw [iInf_inf_eq, iInf_const]

Infimum Distributes Over Meet: $a \sqcap \bigsqcap_x f_x = \bigsqcap_x (a \sqcap f_x)$

Informal description

For any nonempty index type $\iota$, any element $a$ in a complete lattice $\alpha$, and any indexed family of elements $(f_x)_{x \in \iota}$ in $\alpha$, the infimum of $a$ with the infimum of the family equals the infimum of the family obtained by taking the infimum of $a$ with each element of the family, i.e., \[ a \sqcap \left(\bigsqcap_{x} f_x\right) = \bigsqcap_{x} (a \sqcap f_x). \]

biSup_sup theorem

 {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

Full source

theorem biSup_sup {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 := by
  haveI : Nonempty { i // p i } :=
    let ⟨i, hi⟩ := h
    ⟨⟨i, hi⟩⟩
  rw [iSup_subtype', iSup_subtype', iSup_sup]

Bounded Supremum Distributes Over Join: $(\bigsqcup_{i, p(i)} f_i) \sqcup a = \bigsqcup_{i, p(i)} (f_i \sqcup a)$

Informal description

Let $\alpha$ be a complete lattice, $p : \iota \to \mathrm{Prop}$ a predicate on an index type $\iota$, and $f : \forall i, p(i) \to \alpha$ a family of elements in $\alpha$ defined for indices satisfying $p$. For any element $a \in \alpha$ and assuming there exists at least one index $i$ for which $p(i)$ holds, the following equality holds: \[ \left(\bigsqcup_{\substack{i \\ h : p(i)}} f(i, h)\right) \sqcup a = \bigsqcup_{\substack{i \\ h : p(i)}} (f(i, h) \sqcup a). \]

sup_biSup theorem

 {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

Full source

theorem sup_biSup {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 := by
  simpa only [sup_comm] using @biSup_sup α _ _ p _ _ h

Join Distributes Over Bounded Supremum: $a \sqcup (\bigsqcup_{i, p(i)} f_i) = \bigsqcup_{i, p(i)} (a \sqcup f_i)$

Informal description

Let $\alpha$ be a complete lattice, $p : \iota \to \mathrm{Prop}$ a predicate on an index type $\iota$, and $f : \forall i, p(i) \to \alpha$ a family of elements in $\alpha$ defined for indices satisfying $p$. For any element $a \in \alpha$ and assuming there exists at least one index $i$ for which $p(i)$ holds, the following equality holds: \[ a \sqcup \left(\bigsqcup_{\substack{i \\ h : p(i)}} f(i, h)\right) = \bigsqcup_{\substack{i \\ h : p(i)}} (a \sqcup f(i, h)). \]

biInf_inf theorem

 {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

Full source

theorem biInf_inf {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 :=
  @biSup_sup αᵒᵈ ι _ p f _ h

Bounded Infimum Distributes Over Meet: $(\bigsqcap_{i, p(i)} f_i) \sqcap a = \bigsqcap_{i, p(i)} (f_i \sqcap a)$

Informal description

Let $\alpha$ be a complete lattice, $p : \iota \to \mathrm{Prop}$ a predicate on an index type $\iota$, and $f : \forall i, p(i) \to \alpha$ a family of elements in $\alpha$ defined for indices satisfying $p$. For any element $a \in \alpha$ and assuming there exists at least one index $i$ for which $p(i)$ holds, the following equality holds: \[ \left(\bigsqcap_{\substack{i \\ h : p(i)}} f(i, h)\right) \sqcap a = \bigsqcap_{\substack{i \\ h : p(i)}} (f(i, h) \sqcap a). \]

inf_biInf theorem

 {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

Full source

theorem inf_biInf {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 :=
  @sup_biSup αᵒᵈ ι _ p f _ h

Meet Distributes Over Bounded Infimum: $a \sqcap (\bigsqcap_{i, p(i)} f_i) = \bigsqcap_{i, p(i)} (a \sqcap f_i)$

Informal description

Let $\alpha$ be a complete lattice, $p : \iota \to \mathrm{Prop}$ a predicate on an index type $\iota$, and $f : \forall i, p(i) \to \alpha$ a family of elements in $\alpha$ defined for indices satisfying $p$. For any element $a \in \alpha$ and assuming there exists at least one index $i$ for which $p(i)$ holds, the following equality holds: \[ a \sqcap \left(\bigsqcap_{\substack{i \\ h : p(i)}} f(i, h)\right) = \bigsqcap_{\substack{i \\ h : p(i)}} (a \sqcap f(i, h)). \]

biSup_lt_eq_iSup theorem

{ι : Type*} [LT ι] [NoMaxOrder ι] {f : ι → α} : ⨆ (i) (j < i), f j = ⨆ i, f i

Full source

lemma biSup_lt_eq_iSup {ι : Type*} [LT ι] [NoMaxOrder ι] {f : ι → α} :
    ⨆ (i) (j < i), f j = ⨆ i, f i := by
  apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · refine iSup_le fun j ↦ ?_
    obtain ⟨i, jlt⟩ := exists_gt j
    exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

Supremum of Strictly Preceding Elements Equals Supremum in No-Max-Order

Informal description

Let $\iota$ be a type equipped with a strict order relation $<$ and assume $\iota$ has no maximal elements (i.e., for every $i \in \iota$, there exists $j \in \iota$ with $i < j$). For any function $f : \iota \to \alpha$ mapping to a complete lattice $\alpha$, the supremum over all pairs $(i,j)$ with $j < i$ equals the supremum over all $i$: \[ \bigsqcup_{i \in \iota} \bigsqcup_{j < i} f(j) = \bigsqcup_{i \in \iota} f(i). \]

biSup_le_eq_iSup theorem

{ι : Type*} [Preorder ι] {f : ι → α} : ⨆ (i) (j ≤ i), f j = ⨆ i, f i

Full source

lemma biSup_le_eq_iSup {ι : Type*} [Preorder ι] {f : ι → α} :
    ⨆ (i) (j ≤ i), f j = ⨆ i, f i := by
  apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · exact iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

Bounded supremum equals supremum for preordered index sets: $\bigsqcup_{i} \bigsqcup_{j \leq i} f(j) = \bigsqcup_{i} f(i)$

Informal description

Let $\iota$ be a type with a preorder $\leq$ and $\alpha$ be a complete lattice. For any function $f : \iota \to \alpha$, the bounded supremum $\bigsqcup_{i \in \iota} \bigsqcup_{j \leq i} f(j)$ equals the supremum $\bigsqcup_{i \in \iota} f(i)$.

biInf_lt_eq_iInf theorem

{ι : Type*} [LT ι] [NoMaxOrder ι] {f : ι → α} : ⨅ (i) (j < i), f j = ⨅ i, f i

Full source

lemma biInf_lt_eq_iInf {ι : Type*} [LT ι] [NoMaxOrder ι] {f : ι → α} :
    ⨅ (i) (j < i), f j = ⨅ i, f i :=
  biSup_lt_eq_iSup (α := αᵒᵈ)

Infimum of Strictly Preceding Elements Equals Infimum in No-Max-Order

Informal description

Let $\iota$ be a type equipped with a strict order relation $<$ and assume $\iota$ has no maximal elements (i.e., for every $i \in \iota$, there exists $j \in \iota$ with $i < j$). For any function $f : \iota \to \alpha$ mapping to a complete lattice $\alpha$, the infimum over all pairs $(i,j)$ with $j < i$ equals the infimum over all $i$: \[ \bigsqcap_{i \in \iota} \bigsqcap_{j < i} f(j) = \bigsqcap_{i \in \iota} f(i). \]

biInf_le_eq_iInf theorem

{ι : Type*} [Preorder ι] {f : ι → α} : ⨅ (i) (j ≤ i), f j = ⨅ i, f i

Full source

lemma biInf_le_eq_iInf {ι : Type*} [Preorder ι] {f : ι → α} : ⨅ (i) (j ≤ i), f j = ⨅ i, f i :=
  biSup_le_eq_iSup (α := αᵒᵈ)

Bounded infimum equals infimum for preordered index sets: $\bigsqcap_{i} \bigsqcap_{j \leq i} f(j) = \bigsqcap_{i} f(i)$

Informal description

Let $\iota$ be a type with a preorder $\leq$ and $\alpha$ be a complete lattice. For any function $f : \iota \to \alpha$, the bounded infimum $\bigsqcap_{i \in \iota} \bigsqcap_{j \leq i} f(j)$ equals the infimum $\bigsqcap_{i \in \iota} f(i)$.

biSup_gt_eq_iSup theorem

{ι : Type*} [LT ι] [NoMinOrder ι] {f : ι → α} : ⨆ (i) (j > i), f j = ⨆ i, f i

Full source

lemma biSup_gt_eq_iSup {ι : Type*} [LT ι] [NoMinOrder ι] {f : ι → α} :
    ⨆ (i) (j > i), f j = ⨆ i, f i :=
  biSup_lt_eq_iSup (ι := ιᵒᵈ)

Supremum of Strictly Succeeding Elements Equals Supremum in No-Min-Order

Informal description

Let $\iota$ be a type equipped with a strict order relation $<$ and assume $\iota$ has no minimal elements (i.e., for every $i \in \iota$, there exists $j \in \iota$ with $j < i$). For any function $f : \iota \to \alpha$ mapping to a complete lattice $\alpha$, the supremum over all pairs $(i,j)$ with $j > i$ equals the supremum over all $i$: \[ \bigsqcup_{i \in \iota} \bigsqcup_{j > i} f(j) = \bigsqcup_{i \in \iota} f(i). \]

biSup_ge_eq_iSup theorem

{ι : Type*} [Preorder ι] {f : ι → α} : ⨆ (i) (j ≥ i), f j = ⨆ i, f i

Full source

lemma biSup_ge_eq_iSup {ι : Type*} [Preorder ι] {f : ι → α} : ⨆ (i) (j ≥ i), f j = ⨆ i, f i :=
  biSup_le_eq_iSup (ι := ιᵒᵈ)

Bounded supremum equals supremum for non-decreasing sequences: $\bigsqcup_{i} \bigsqcup_{j \geq i} f(j) = \bigsqcup_{i} f(i)$

Informal description

Let $\iota$ be a type with a preorder $\leq$ and $\alpha$ be a complete lattice. For any function $f : \iota \to \alpha$, the bounded supremum $\bigsqcup_{i \in \iota} \bigsqcup_{j \geq i} f(j)$ equals the supremum $\bigsqcup_{i \in \iota} f(i)$.

biInf_gt_eq_iInf theorem

{ι : Type*} [LT ι] [NoMinOrder ι] {f : ι → α} : ⨅ (i) (j > i), f j = ⨅ i, f i

Full source

lemma biInf_gt_eq_iInf {ι : Type*} [LT ι] [NoMinOrder ι] {f : ι → α} :
    ⨅ (i) (j > i), f j = ⨅ i, f i :=
  biInf_lt_eq_iInf (ι := ιᵒᵈ)

Infimum of Strictly Succeeding Elements Equals Infimum in No-Min-Order

Informal description

Let $\iota$ be a type equipped with a strict order relation $<$ and assume $\iota$ has no minimal elements (i.e., for every $i \in \iota$, there exists $j \in \iota$ with $j < i$). For any function $f : \iota \to \alpha$ mapping to a complete lattice $\alpha$, the infimum over all pairs $(i,j)$ with $j > i$ equals the infimum over all $i$: \[ \bigsqcap_{i \in \iota} \bigsqcap_{j > i} f(j) = \bigsqcap_{i \in \iota} f(i). \]

biInf_ge_eq_iInf theorem

{ι : Type*} [Preorder ι] {f : ι → α} : ⨅ (i) (j ≥ i), f j = ⨅ i, f i

Full source

lemma biInf_ge_eq_iInf {ι : Type*} [Preorder ι] {f : ι → α} : ⨅ (i) (j ≥ i), f j = ⨅ i, f i :=
  biInf_le_eq_iInf (ι := ιᵒᵈ)

Bounded infimum equals infimum for non-increasing sequences: $\bigsqcap_i \bigsqcap_{j \geq i} f(j) = \bigsqcap_i f(i)$

Informal description

Let $\iota$ be a type equipped with a preorder $\leq$ and $\alpha$ be a complete lattice. For any function $f : \iota \to \alpha$, the bounded infimum $\bigsqcap_{i \in \iota} \bigsqcap_{j \geq i} f(j)$ equals the infimum $\bigsqcap_{i \in \iota} f(i)$.

biSup_le_eq_of_monotone theorem

[Preorder β] {f : β → α} (hf : Monotone f) (b : β) : ⨆ (b' ≤ b), f b' = f b

Full source

lemma biSup_le_eq_of_monotone [Preorder β] {f : β → α} (hf : Monotone f) (b : β) :
    ⨆ (b' ≤ b), f b' = f b :=
  le_antisymm (iSup₂_le_iff.2 (fun _ hji ↦ hf hji))
    (le_iSup_of_le b (ge_of_eq (iSup_pos le_rfl)))

Supremum of Monotone Function over Lower Set Equals Function Value

Informal description

Let $\beta$ be a preorder and $\alpha$ be a complete lattice. For any monotone function $f : \beta \to \alpha$ and any element $b \in \beta$, the supremum of $f$ over all elements $b' \leq b$ equals $f(b)$, i.e., \[ \bigsqcup_{b' \leq b} f(b') = f(b). \]

biInf_le_eq_of_antitone theorem

[Preorder β] {f : β → α} (hf : Antitone f) (b : β) : ⨅ (b' ≤ b), f b' = f b

Full source

lemma biInf_le_eq_of_antitone [Preorder β] {f : β → α} (hf : Antitone f) (b : β) :
    ⨅ (b' ≤ b), f b' = f b :=
  biSup_le_eq_of_monotone (α := αᵒᵈ) hf.dual_right b

Infimum of Antitone Function over Lower Set Equals Function Value

Informal description

Let $\alpha$ be a complete lattice and $\beta$ be a preorder. For any antitone function $f : \beta \to \alpha$ and any element $b \in \beta$, the infimum of $f$ over all elements $b' \leq b$ equals $f(b)$, i.e., \[ \bigsqcap_{b' \leq b} f(b') = f(b). \]

biSup_ge_eq_of_antitone theorem

[Preorder β] {f : β → α} (hf : Antitone f) (b : β) : ⨆ (b' ≥ b), f b' = f b

Full source

lemma biSup_ge_eq_of_antitone [Preorder β] {f : β → α} (hf : Antitone f) (b : β) :
    ⨆ (b' ≥ b), f b' = f b :=
  biSup_le_eq_of_monotone (β := βᵒᵈ) hf.dual_left b

Supremum of Antitone Function over Upper Set Equals Function Value

Informal description

Let $\alpha$ be a complete lattice and $\beta$ be a preorder. For any antitone function $f : \beta \to \alpha$ and any element $b \in \beta$, the supremum of $f$ over all elements $b' \geq b$ equals $f(b)$, i.e., \[ \bigsqcup_{b' \geq b} f(b') = f(b). \]

biInf_ge_eq_of_monotone theorem

[Preorder β] {f : β → α} (hf : Monotone f) (b : β) : ⨅ (b' ≥ b), f b' = f b

Full source

lemma biInf_ge_eq_of_monotone [Preorder β] {f : β → α} (hf : Monotone f) (b : β) :
    ⨅ (b' ≥ b), f b' = f b :=
  biInf_le_eq_of_antitone (β := βᵒᵈ) hf.dual_left b

Infimum of Monotone Function over Upper Set Equals Function Value

Informal description

Let $\alpha$ be a complete lattice and $\beta$ be a preorder. For any monotone function $f : \beta \to \alpha$ and any element $b \in \beta$, the infimum of $f$ over all elements $b' \geq b$ equals $f(b)$, i.e., \[ \bigsqcap_{b' \geq b} f(b') = f(b). \]

iSup_false theorem

{s : False → α} : iSup s = ⊥

Full source

theorem iSup_false {s : False → α} : iSup s = ⊥ := by simp

Supremum over Empty Type is Bottom Element

Informal description

For any function $s$ from the empty type (False) to a complete lattice $\alpha$, the supremum of $s$ is equal to the bottom element $\bot$ of $\alpha$. That is, $\bigsqcup_{x : \text{False}} s(x) = \bot$.

iInf_false theorem

{s : False → α} : iInf s = ⊤

Full source

theorem iInf_false {s : False → α} : iInf s = ⊤ := by simp

Infimum over False is Top

Informal description

For any function $s$ from the empty type `False` to a complete lattice $\alpha$, the infimum of $s$ is equal to the top element $\top$ of $\alpha$, i.e., $\bigsqcap_{x : \text{False}} s(x) = \top$.

iSup_true theorem

{s : True → α} : iSup s = s trivial

Full source

theorem iSup_true {s : True → α} : iSup s = s trivial :=
  iSup_pos trivial

Supremum over True Proposition Equals Function Value at Trivial Proof

Informal description

For any function $s$ from the true proposition $\text{True}$ to a complete lattice $\alpha$, the supremum of $s$ over all proofs of $\text{True}$ equals $s(\text{trivial})$, where $\text{trivial}$ is the canonical proof of $\text{True}$. That is, $\bigsqcup_{x : \text{True}} s(x) = s(\text{trivial})$.

iInf_true theorem

{s : True → α} : iInf s = s trivial

Full source

theorem iInf_true {s : True → α} : iInf s = s trivial :=
  iInf_pos trivial

Infimum over True equals its value at trivial

Informal description

For any complete lattice $\alpha$ and any function $s : \text{True} \to \alpha$, the infimum $\bigsqcap_{x : \text{True}} s(x)$ equals $s(\text{trivial})$, where $\text{trivial}$ is the canonical proof of $\text{True}$.

iSup_exists theorem

{p : ι → Prop} {f : Exists p → α} : ⨆ x, f x = ⨆ (i) (h), f ⟨i, h⟩

Full source

@[simp]
theorem iSup_exists {p : ι → Prop} {f : Exists p → α} : ⨆ x, f x = ⨆ (i) (h), f ⟨i, h⟩ :=
  le_antisymm (iSup_le fun ⟨i, h⟩ => @le_iSup₂ _ _ _ _ (fun _ _ => _) i h)
    (iSup₂_le fun _ _ => le_iSup _ _)

Supremum over Existential Quantifier Equals Double Supremum

Informal description

For any predicate $p : \iota \to \text{Prop}$ and any function $f : \text{Exists } p \to \alpha$ from the existential type $\text{Exists } p$ to a complete lattice $\alpha$, the supremum of $f$ over all proofs of $\text{Exists } p$ is equal to the double supremum over all indices $i \in \iota$ and proofs $h : p(i)$ of $f$ evaluated at the pair $\langle i, h \rangle$. That is, \[ \bigsqcup_{x : \text{Exists } p} f(x) = \bigsqcup_{i \in \iota} \bigsqcup_{h : p(i)} f(\langle i, h \rangle). \]

iInf_exists theorem

{p : ι → Prop} {f : Exists p → α} : ⨅ x, f x = ⨅ (i) (h), f ⟨i, h⟩

Full source

@[simp]
theorem iInf_exists {p : ι → Prop} {f : Exists p → α} : ⨅ x, f x = ⨅ (i) (h), f ⟨i, h⟩ :=
  @iSup_exists αᵒᵈ _ _ _ _

Infimum over Existential Quantifier Equals Double Infimum

Informal description

For any predicate $p : \iota \to \text{Prop}$ and any function $f : \text{Exists } p \to \alpha$ from the existential type $\text{Exists } p$ to a complete lattice $\alpha$, the infimum of $f$ over all proofs of $\text{Exists } p$ is equal to the double infimum over all indices $i \in \iota$ and proofs $h : p(i)$ of $f$ evaluated at the pair $\langle i, h \rangle$. That is, \[ \bigsqcap_{x : \text{Exists } p} f(x) = \bigsqcap_{i \in \iota} \bigsqcap_{h : p(i)} f(\langle i, h \rangle). \]

iSup_and theorem

{p q : Prop} {s : p ∧ q → α} : iSup s = ⨆ (h₁) (h₂), s ⟨h₁, h₂⟩

Full source

theorem iSup_and {p q : Prop} {s : p ∧ q → α} : iSup s = ⨆ (h₁) (h₂), s ⟨h₁, h₂⟩ :=
  le_antisymm (iSup_le fun ⟨i, h⟩ => @le_iSup₂ _ _ _ _ (fun _ _ => _) i h)
    (iSup₂_le fun _ _ => le_iSup _ _)

Supremum over Conjunction Equals Double Supremum

Informal description

For any two propositions $p$ and $q$ and any function $s : p \land q \to \alpha$ from the conjunction of $p$ and $q$ to a complete lattice $\alpha$, the supremum of $s$ over all proofs of $p \land q$ is equal to the double supremum of $s$ over all proofs of $p$ and all proofs of $q$. That is, \[ \bigsqcup_{h : p \land q} s(h) = \bigsqcup_{h_1 : p} \bigsqcup_{h_2 : q} s(\langle h_1, h_2 \rangle). \]

iInf_and theorem

{p q : Prop} {s : p ∧ q → α} : iInf s = ⨅ (h₁) (h₂), s ⟨h₁, h₂⟩

Full source

theorem iInf_and {p q : Prop} {s : p ∧ q → α} : iInf s = ⨅ (h₁) (h₂), s ⟨h₁, h₂⟩ :=
  @iSup_and αᵒᵈ _ _ _ _

Infimum over Conjunction Equals Double Infimum

Informal description

For any two propositions $p$ and $q$ and any function $s : p \land q \to \alpha$ from the conjunction of $p$ and $q$ to a complete lattice $\alpha$, the infimum of $s$ over all proofs of $p \land q$ is equal to the double infimum of $s$ over all proofs of $p$ and all proofs of $q$. That is, \[ \bigsqcap_{h : p \land q} s(h) = \bigsqcap_{h_1 : p} \bigsqcap_{h_2 : q} s(\langle h_1, h_2 \rangle). \]

iSup_and' theorem

{p q : Prop} {s : p → q → α} : ⨆ (h₁ : p) (h₂ : q), s h₁ h₂ = ⨆ h : p ∧ q, s h.1 h.2

Full source

/-- The symmetric case of `iSup_and`, useful for rewriting into a supremum over a conjunction -/
theorem iSup_and' {p q : Prop} {s : p → q → α} :
    ⨆ (h₁ : p) (h₂ : q), s h₁ h₂ = ⨆ h : p ∧ q, s h.1 h.2 :=
  Eq.symm iSup_and

Double Supremum over Propositions Equals Supremum over Conjunction

Informal description

For any two propositions $p$ and $q$ and any function $s : p \to q \to \alpha$ from $p$ and $q$ to a complete lattice $\alpha$, the double supremum of $s$ over all proofs of $p$ and all proofs of $q$ is equal to the supremum of $s$ over all proofs of the conjunction $p \land q$. That is, \[ \bigsqcup_{h_1 : p} \bigsqcup_{h_2 : q} s(h_1, h_2) = \bigsqcup_{h : p \land q} s(h.1, h.2). \]

iInf_and' theorem

{p q : Prop} {s : p → q → α} : ⨅ (h₁ : p) (h₂ : q), s h₁ h₂ = ⨅ h : p ∧ q, s h.1 h.2

Full source

/-- The symmetric case of `iInf_and`, useful for rewriting into an infimum over a conjunction -/
theorem iInf_and' {p q : Prop} {s : p → q → α} :
    ⨅ (h₁ : p) (h₂ : q), s h₁ h₂ = ⨅ h : p ∧ q, s h.1 h.2 :=
  Eq.symm iInf_and

Double Infimum over Propositions Equals Infimum over Conjunction

Informal description

For any two propositions $p$ and $q$ and any function $s : p \to q \to \alpha$ from $p$ and $q$ to a complete lattice $\alpha$, the double infimum of $s$ over all proofs of $p$ and all proofs of $q$ is equal to the infimum of $s$ over all proofs of the conjunction $p \land q$. That is, \[ \bigsqcap_{h_1 : p} \bigsqcap_{h_2 : q} s(h_1, h_2) = \bigsqcap_{h : p \land q} s(h.1, h.2). \]

iSup_or theorem

{p q : Prop} {s : p ∨ q → α} : ⨆ x, s x = (⨆ i, s (Or.inl i)) ⊔ ⨆ j, s (Or.inr j)

Full source

theorem iSup_or {p q : Prop} {s : p ∨ q → α} :
    ⨆ x, s x = (⨆ i, s (Or.inl i)) ⊔ ⨆ j, s (Or.inr j) :=
  le_antisymm
    (iSup_le fun i =>
      match i with
      | Or.inl _ => le_sup_of_le_left <| le_iSup (fun _ => s _) _
      | Or.inr _ => le_sup_of_le_right <| le_iSup (fun _ => s _) _)
    (sup_le (iSup_comp_le _ _) (iSup_comp_le _ _))

Supremum over Disjunction Equals Join of Suprema over Each Case

Informal description

For any indexed family of elements $s : p \lor q \to \alpha$ in a complete lattice $\alpha$, where $p$ and $q$ are propositions, the supremum of $s$ over all possible values is equal to the supremum of $s$ over the left injections $\Or.inl$ (i.e., when $p$ holds) joined with the supremum of $s$ over the right injections $\Or.inr$ (i.e., when $q$ holds). In other words: \[ \bigsqcup_{x \in p \lor q} s(x) = \left(\bigsqcup_{i \in p} s(\Or.inl\, i)\right) \sqcup \left(\bigsqcup_{j \in q} s(\Or.inr\, j)\right). \]

iInf_or theorem

{p q : Prop} {s : p ∨ q → α} : ⨅ x, s x = (⨅ i, s (Or.inl i)) ⊓ ⨅ j, s (Or.inr j)

Full source

theorem iInf_or {p q : Prop} {s : p ∨ q → α} :
    ⨅ x, s x = (⨅ i, s (Or.inl i)) ⊓ ⨅ j, s (Or.inr j) :=
  @iSup_or αᵒᵈ _ _ _ _

Infimum over Disjunction Equals Meet of Infima over Each Case

Informal description

For any complete lattice $\alpha$ and any indexed family of elements $s : p \lor q \to \alpha$ where $p$ and $q$ are propositions, the infimum of $s$ over all values is equal to the infimum of $s$ over the left case (when $p$ holds) meet with the infimum of $s$ over the right case (when $q$ holds). In symbols: \[ \bigsqcap_{x \in p \lor q} s(x) = \left(\bigsqcap_{i \in p} s(\text{Or.inl}\, i)\right) \sqcap \left(\bigsqcap_{j \in q} s(\text{Or.inr}\, j)\right). \]

iSup_dite theorem

 (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

Full source

theorem iSup_dite (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 := by
  rw [← iSup_sup_eq]
  congr 1 with i
  split_ifs with h <;> simp [h]

Supremum of Dependent If-Then-Else Equals Supremum of Cases

Informal description

Let $\alpha$ be a complete lattice, and let $p$ be a predicate on an index set $\iota$. For any two families of elements $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ in $\alpha$ defined respectively for indices where $p$ holds and where $p$ does not hold, the supremum of the dependent if-then-else expression equals the supremum of the $f_i$ (over indices where $p$ holds) joined with the supremum of the $g_i$ (over indices where $p$ does not hold). That is, \[ \bigsqcup_{i} \left( \text{if } h : p(i) \text{ then } f_i h \text{ else } g_i h \right) = \left( \bigsqcup_{\substack{i \\ h : p(i)}} f_i h \right) \sqcup \left( \bigsqcup_{\substack{i \\ h : \neg p(i)}} g_i h \right). \]

iInf_dite theorem

 (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

Full source

theorem iInf_dite (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 :=
  iSup_dite p (show ∀ i, p i → αᵒᵈ from f) g

Infimum of Dependent If-Then-Else Equals Infimum of Cases

Informal description

Let $\alpha$ be a complete lattice, and let $p$ be a predicate on an index set $\iota$. For any two families of elements $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ in $\alpha$ defined respectively for indices where $p$ holds and where $p$ does not hold, the infimum of the dependent if-then-else expression equals the infimum of the $f_i$ (over indices where $p$ holds) meet with the infimum of the $g_i$ (over indices where $p$ does not hold). That is, \[ \bigsqcap_{i} \left( \text{if } h : p(i) \text{ then } f_i h \text{ else } g_i h \right) = \left( \bigsqcap_{\substack{i \\ h : p(i)}} f_i h \right) \sqcap \left( \bigsqcap_{\substack{i \\ h : \neg p(i)}} g_i h \right). \]

iSup_ite theorem

(f g : ι → α) : ⨆ i, (if p i then f i else g i) = (⨆ (i) (_ : p i), f i) ⊔ ⨆ (i) (_ : ¬p i), g i

Full source

theorem iSup_ite (f g : ι → α) :
    ⨆ i, (if p i then f i else g i) = (⨆ (i) (_ : p i), f i) ⊔ ⨆ (i) (_ : ¬p i), g i :=
  iSup_dite _ _ _

Supremum of If-Then-Else Equals Supremum of Cases

Informal description

Let $\alpha$ be a complete lattice, and let $p$ be a predicate on an index set $\iota$. For any two families of elements $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ in $\alpha$, the supremum of the if-then-else expression equals the supremum of the $f_i$ (over indices where $p$ holds) joined with the supremum of the $g_i$ (over indices where $p$ does not hold). That is, \[ \bigsqcup_{i} \left( \text{if } p(i) \text{ then } f_i \text{ else } g_i \right) = \left( \bigsqcup_{\substack{i \\ p(i)}} f_i \right) \sqcup \left( \bigsqcup_{\substack{i \\ \neg p(i)}} g_i \right). \]

iInf_ite theorem

(f g : ι → α) : ⨅ i, (if p i then f i else g i) = (⨅ (i) (_ : p i), f i) ⊓ ⨅ (i) (_ : ¬p i), g i

Full source

theorem iInf_ite (f g : ι → α) :
    ⨅ i, (if p i then f i else g i) = (⨅ (i) (_ : p i), f i) ⊓ ⨅ (i) (_ : ¬p i), g i :=
  iInf_dite _ _ _

Infimum of If-Then-Else Equals Infimum of Cases

Informal description

Let $\alpha$ be a complete lattice, and let $p$ be a predicate on an index set $\iota$. For any two families of elements $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ in $\alpha$, the infimum of the if-then-else expression equals the infimum of the $f_i$ (over indices where $p$ holds) meet with the infimum of the $g_i$ (over indices where $p$ does not hold). That is, \[ \bigsqcap_{i} \left( \text{if } p(i) \text{ then } f_i \text{ else } g_i \right) = \left( \bigsqcap_{\substack{i \\ p(i)}} f_i \right) \sqcap \left( \bigsqcap_{\substack{i \\ \neg p(i)}} g_i \right). \]

iSup_range theorem

{g : β → α} {f : ι → β} : ⨆ b ∈ range f, g b = ⨆ i, g (f i)

Full source

theorem iSup_range {g : β → α} {f : ι → β} : ⨆ b ∈ range f, g b = ⨆ i, g (f i) := by
  rw [← iSup_subtype'', iSup_range']

Supremum over Range Equals Supremum of Composition: $\bigsqcup_{\mathrm{range}(f)} g = \bigsqcup_i g(f(i))$

Informal description

For any functions $g : \beta \to \alpha$ and $f : \iota \to \beta$, the supremum of $g$ over the range of $f$ equals the supremum of the composition $g \circ f$ over the index set $\iota$. In symbols: $$\bigsqcup_{b \in \mathrm{range}(f)} g(b) = \bigsqcup_{i \in \iota} g(f(i)).$$

iInf_range theorem

: ∀ {g : β → α} {f : ι → β}, ⨅ b ∈ range f, g b = ⨅ i, g (f i)

Full source

theorem iInf_range : ∀ {g : β → α} {f : ι → β}, ⨅ b ∈ range f, g b = ⨅ i, g (f i) :=
  @iSup_range αᵒᵈ _ _ _

Infimum over Range Equals Infimum of Composition: $\bigsqcap_{\mathrm{range}(f)} g = \bigsqcap_i g(f(i))$

Informal description

For any functions $g : \beta \to \alpha$ and $f : \iota \to \beta$, the infimum of $g$ over the range of $f$ equals the infimum of the composition $g \circ f$ over the index set $\iota$. In symbols: $$\bigsqcap_{b \in \mathrm{range}(f)} g(b) = \bigsqcap_{i \in \iota} g(f(i)).$$

sSup_image theorem

{s : Set β} {f : β → α} : sSup (f '' s) = ⨆ a ∈ s, f a

Full source

theorem sSup_image {s : Set β} {f : β → α} : sSup (f '' s) = ⨆ a ∈ s, f a := by
  rw [← iSup_subtype'', sSup_image']

Supremum of Image Equals Bounded Supremum

Informal description

For any set $s \subseteq \beta$ and any function $f : \beta \to \alpha$, the supremum of the image of $s$ under $f$ equals the supremum of $f(a)$ over all $a \in s$, i.e., $$\sup f(s) = \bigsqcup_{a \in s} f(a).$$

sInf_image theorem

{s : Set β} {f : β → α} : sInf (f '' s) = ⨅ a ∈ s, f a

Full source

theorem sInf_image {s : Set β} {f : β → α} : sInf (f '' s) = ⨅ a ∈ s, f a :=
  @sSup_image αᵒᵈ _ _ _ _

Infimum of Image Equals Bounded Infimum

Informal description

For any set $s \subseteq \beta$ and any function $f : \beta \to \alpha$, the infimum of the image of $s$ under $f$ equals the infimum of $f(a)$ over all $a \in s$, i.e., $$\inf f(s) = \bigsqcap_{a \in s} f(a).$$

OrderIso.map_sSup_eq_sSup_symm_preimage theorem

[CompleteLattice β] (f : α ≃o β) (s : Set α) : f (sSup s) = sSup (f.symm ⁻¹' s)

Full source

theorem OrderIso.map_sSup_eq_sSup_symm_preimage [CompleteLattice β] (f : α ≃o β) (s : Set α) :
    f (sSup s) = sSup (f.symm ⁻¹' s) := by
  rw [map_sSup, ← sSup_image, f.image_eq_preimage]

Order Isomorphism Maps Supremum to Supremum of Inverse Preimage

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \simeq_o \beta$ be an order isomorphism. For any subset $s \subseteq \alpha$, the image under $f$ of the supremum of $s$ equals the supremum of the preimage of $s$ under the inverse isomorphism $f^{-1}$, i.e., \[ f\left(\bigvee s\right) = \bigvee f^{-1}(s). \]

OrderIso.map_sInf_eq_sInf_symm_preimage theorem

[CompleteLattice β] (f : α ≃o β) (s : Set α) : f (sInf s) = sInf (f.symm ⁻¹' s)

Full source

theorem OrderIso.map_sInf_eq_sInf_symm_preimage [CompleteLattice β] (f : α ≃o β) (s : Set α) :
    f (sInf s) = sInf (f.symm ⁻¹' s) := by
  rw [map_sInf, ← sInf_image, f.image_eq_preimage]

Order Isomorphism Maps Infimum to Infimum of Inverse Preimage

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \simeq_o \beta$ be an order isomorphism. For any subset $s \subseteq \alpha$, the image under $f$ of the infimum of $s$ equals the infimum of the preimage of $s$ under the inverse isomorphism $f^{-1}$, i.e., \[ f\left(\bigwedge s\right) = \bigwedge f^{-1}(s). \]

iSup_emptyset theorem

{f : β → α} : ⨆ x ∈ (∅ : Set β), f x = ⊥

Full source

theorem iSup_emptyset {f : β → α} : ⨆ x ∈ (∅ : Set β), f x = ⊥ := by simp

Supremum over Empty Set is Bottom Element

Informal description

For any function $f : \beta \to \alpha$ where $\alpha$ is a complete lattice, the supremum of $f$ over the empty set is equal to the bottom element $\bot$ of $\alpha$. That is, \[ \bigsqcup_{x \in \emptyset} f(x) = \bot. \]

iInf_emptyset theorem

{f : β → α} : ⨅ x ∈ (∅ : Set β), f x = ⊤

Full source

theorem iInf_emptyset {f : β → α} : ⨅ x ∈ (∅ : Set β), f x = ⊤ := by simp

Infimum over Empty Set Equals Top Element

Informal description

For any function $f : \beta \to \alpha$ mapping into a complete lattice $\alpha$, the infimum of $f$ over the empty set is equal to the top element $\top$ of $\alpha$, i.e., \[ \bigsqcap_{x \in \emptyset} f(x) = \top. \]

iSup_univ theorem

{f : β → α} : ⨆ x ∈ (univ : Set β), f x = ⨆ x, f x

Full source

theorem iSup_univ {f : β → α} : ⨆ x ∈ (univ : Set β), f x = ⨆ x, f x := by simp

Supremum over Universal Set Equals Unbounded Supremum

Informal description

For any function $f : \beta \to \alpha$ where $\alpha$ is a complete lattice, the supremum of $f$ over the universal set (all elements of $\beta$) equals the supremum of $f$ over all elements of $\beta$. That is, \[ \bigsqcup_{x \in \beta} f(x) = \bigsqcup_{x} f(x). \]

iInf_univ theorem

{f : β → α} : ⨅ x ∈ (univ : Set β), f x = ⨅ x, f x

Full source

theorem iInf_univ {f : β → α} : ⨅ x ∈ (univ : Set β), f x = ⨅ x, f x := by simp

Infimum over Universal Set Equals Global Infimum

Informal description

For any function $f : \beta \to \alpha$ mapping into a complete lattice $\alpha$, the infimum of $f$ over the universal set (the set of all elements of $\beta$) equals the infimum of $f$ over the entire domain, i.e., \[ \bigsqcap_{x \in \beta} f(x) = \bigsqcap_{x} f(x). \]

iSup_union theorem

{f : β → α} {s t : Set β} : ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Full source

theorem iSup_union {f : β → α} {s t : Set β} :
    ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x := by
  simp_rw [mem_union, iSup_or, iSup_sup_eq]

Supremum over Union Equals Join of Suprema

Informal description

For any function $f : \beta \to \alpha$ mapping into a complete lattice $\alpha$, and for any sets $s, t \subseteq \beta$, the supremum of $f$ over the union $s \cup t$ equals the join of the suprema of $f$ over $s$ and $t$ individually. That is, \[ \bigsqcup_{x \in s \cup t} f(x) = \left(\bigsqcup_{x \in s} f(x)\right) \sqcup \left(\bigsqcup_{x \in t} f(x)\right). \]

iInf_union theorem

{f : β → α} {s t : Set β} : ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x

Full source

theorem iInf_union {f : β → α} {s t : Set β} : ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x :=
  @iSup_union αᵒᵈ _ _ _ _ _

Infimum over Union Equals Meet of Infima

Informal description

For any function $f : \beta \to \alpha$ mapping into a complete lattice $\alpha$, and for any sets $s, t \subseteq \beta$, the infimum of $f$ over the union $s \cup t$ equals the meet of the infima of $f$ over $s$ and $t$ individually. That is, \[ \bigsqcap_{x \in s \cup t} f(x) = \left(\bigsqcap_{x \in s} f(x)\right) \sqcap \left(\bigsqcap_{x \in t} f(x)\right). \]

iSup_split theorem

(f : β → α) (p : β → Prop) : ⨆ i, f i = (⨆ (i) (_ : p i), f i) ⊔ ⨆ (i) (_ : ¬p i), f i

Full source

theorem iSup_split (f : β → α) (p : β → Prop) :
    ⨆ i, f i = (⨆ (i) (_ : p i), f i) ⊔ ⨆ (i) (_ : ¬p i), f i := by
  simpa [Classical.em] using @iSup_union _ _ _ f { i | p i } { i | ¬p i }

Supremum Splitting over Predicate: $\bigsqcup_i f(i) = (\bigsqcup_{p i} f(i)) \sqcup (\bigsqcup_{\neg p i} f(i))$

Informal description

For any function $f : \beta \to \alpha$ mapping into a complete lattice $\alpha$ and any predicate $p : \beta \to \mathrm{Prop}$, the supremum of $f$ over all indices $i \in \beta$ equals the join of the suprema of $f$ over the indices satisfying $p$ and those not satisfying $p$. That is, \[ \bigsqcup_{i} f(i) = \left(\bigsqcup_{\substack{i \\ p i}} f(i)\right) \sqcup \left(\bigsqcup_{\substack{i \\ \neg p i}} f(i)\right). \]

iInf_split theorem

: ∀ (f : β → α) (p : β → Prop), ⨅ i, f i = (⨅ (i) (_ : p i), f i) ⊓ ⨅ (i) (_ : ¬p i), f i

Full source

theorem iInf_split :
    ∀ (f : β → α) (p : β → Prop), ⨅ i, f i = (⨅ (i) (_ : p i), f i) ⊓ ⨅ (i) (_ : ¬p i), f i :=
  @iSup_split αᵒᵈ _ _

Infimum Splitting over Predicate: $\bigsqcap_i f(i) = (\bigsqcap_{p i} f(i)) \sqcap (\bigsqcap_{\neg p i} f(i))$

Informal description

For any function $f \colon \beta \to \alpha$ mapping into a complete lattice $\alpha$ and any predicate $p \colon \beta \to \mathrm{Prop}$, the infimum of $f$ over all indices $i \in \beta$ equals the meet of the infima of $f$ over the indices satisfying $p$ and those not satisfying $p$. That is, \[ \bigsqcap_{i} f(i) = \left(\bigsqcap_{\substack{i \\ p i}} f(i)\right) \sqcap \left(\bigsqcap_{\substack{i \\ \neg p i}} f(i)\right). \]

iSup_split_single theorem

(f : β → α) (i₀ : β) : ⨆ i, f i = f i₀ ⊔ ⨆ (i) (_ : i ≠ i₀), f i

Full source

theorem iSup_split_single (f : β → α) (i₀ : β) : ⨆ i, f i = f i₀ ⊔ ⨆ (i) (_ : i ≠ i₀), f i := by
  convert iSup_split f (fun i => i = i₀)
  simp

Supremum Splitting at a Single Index: $\bigsqcup_i f(i) = f(i_0) \sqcup \bigsqcup_{i \neq i_0} f(i)$

Informal description

For any function $f \colon \beta \to \alpha$ mapping into a complete lattice $\alpha$ and any distinguished element $i_0 \in \beta$, the supremum of $f$ over all indices $i \in \beta$ equals the join of $f(i_0)$ with the supremum of $f$ over all indices $i \neq i_0$. That is, \[ \bigsqcup_{i \in \beta} f(i) = f(i_0) \sqcup \left(\bigsqcup_{\substack{i \in \beta \\ i \neq i_0}} f(i)\right). \]

iInf_split_single theorem

(f : β → α) (i₀ : β) : ⨅ i, f i = f i₀ ⊓ ⨅ (i) (_ : i ≠ i₀), f i

Full source

theorem iInf_split_single (f : β → α) (i₀ : β) : ⨅ i, f i = f i₀ ⊓ ⨅ (i) (_ : i ≠ i₀), f i :=
  @iSup_split_single αᵒᵈ _ _ _ _

Infimum Splitting at a Single Index: $\bigsqcap_i f(i) = f(i_0) \sqcap \bigsqcap_{i \neq i_0} f(i)$

Informal description

For any function $f \colon \beta \to \alpha$ mapping into a complete lattice $\alpha$ and any distinguished element $i_0 \in \beta$, the infimum of $f$ over all indices $i \in \beta$ equals the meet of $f(i_0)$ with the infimum of $f$ over all indices $i \neq i_0$. That is, \[ \bigsqcap_{i \in \beta} f(i) = f(i_0) \sqcap \left(\bigsqcap_{\substack{i \in \beta \\ i \neq i_0}} f(i)\right). \]

iSup_le_iSup_of_subset theorem

{f : β → α} {s t : Set β} : s ⊆ t → ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x

Full source

theorem iSup_le_iSup_of_subset {f : β → α} {s t : Set β} : s ⊆ t → ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x :=
  biSup_mono

Monotonicity of Supremum under Subset Inclusion

Informal description

For any function $f \colon \beta \to \alpha$ where $\alpha$ is a complete lattice, and any subsets $s, t \subseteq \beta$ such that $s \subseteq t$, the supremum of $f$ over $s$ is less than or equal to the supremum of $f$ over $t$. In symbols: \[ \bigsqcup_{x \in s} f(x) \leq \bigsqcup_{x \in t} f(x) \]

iInf_le_iInf_of_subset theorem

{f : β → α} {s t : Set β} : s ⊆ t → ⨅ x ∈ t, f x ≤ ⨅ x ∈ s, f x

Full source

theorem iInf_le_iInf_of_subset {f : β → α} {s t : Set β} : s ⊆ t → ⨅ x ∈ t, f x ≤ ⨅ x ∈ s, f x :=
  biInf_mono

Monotonicity of Infimum under Subset Inclusion: $\bigsqcap_{t} f \leq \bigsqcap_{s} f$ when $s \subseteq t$

Informal description

For any complete lattice $\alpha$, any function $f : \beta \to \alpha$, and any subsets $s, t \subseteq \beta$ such that $s \subseteq t$, the infimum of $f$ over $t$ is less than or equal to the infimum of $f$ over $s$. In symbols: \[ \bigsqcap_{x \in t} f(x) \leq \bigsqcap_{x \in s} f(x) \]

iSup_insert theorem

{f : β → α} {s : Set β} {b : β} : ⨆ x ∈ insert b s, f x = f b ⊔ ⨆ x ∈ s, f x

Full source

theorem iSup_insert {f : β → α} {s : Set β} {b : β} :
    ⨆ x ∈ insert b s, f x = f b ⊔ ⨆ x ∈ s, f x :=
  Eq.trans iSup_union <| congr_arg (fun x => x ⊔ ⨆ x ∈ s, f x) iSup_iSup_eq_left

Supremum over Inserted Element: $\bigsqcup_{x \in \{b\} \cup s} f(x) = f(b) \sqcup \bigsqcup_{x \in s} f(x)$

Informal description

For any function $f \colon \beta \to \alpha$ where $\alpha$ is a complete lattice, any subset $s \subseteq \beta$, and any element $b \in \beta$, the supremum of $f$ over the set $\{b\} \cup s$ equals the join of $f(b)$ and the supremum of $f$ over $s$. In symbols: \[ \bigsqcup_{x \in \{b\} \cup s} f(x) = f(b) \sqcup \left(\bigsqcup_{x \in s} f(x)\right). \]

iInf_insert theorem

{f : β → α} {s : Set β} {b : β} : ⨅ x ∈ insert b s, f x = f b ⊓ ⨅ x ∈ s, f x

Full source

theorem iInf_insert {f : β → α} {s : Set β} {b : β} :
    ⨅ x ∈ insert b s, f x = f b ⊓ ⨅ x ∈ s, f x :=
  Eq.trans iInf_union <| congr_arg (fun x => x ⊓ ⨅ x ∈ s, f x) iInf_iInf_eq_left

Infimum over Inserted Element: $\bigsqcap_{\{b\} \cup s} f = f(b) \sqcap \bigsqcap_s f$

Informal description

For any function $f \colon \beta \to \alpha$ where $\alpha$ is a complete lattice, any subset $s \subseteq \beta$, and any element $b \in \beta$, the infimum of $f$ over the set $\{b\} \cup s$ equals the meet of $f(b)$ and the infimum of $f$ over $s$. In symbols: \[ \bigsqcap_{x \in \{b\} \cup s} f(x) = f(b) \sqcap \left(\bigsqcap_{x \in s} f(x)\right). \]

iSup_singleton theorem

{f : β → α} {b : β} : ⨆ x ∈ (singleton b : Set β), f x = f b

Full source

theorem iSup_singleton {f : β → α} {b : β} : ⨆ x ∈ (singleton b : Set β), f x = f b := by simp

Supremum over a Singleton Set: $\bigsqcup_{x \in \{b\}} f(x) = f(b)$

Informal description

For any function $f \colon \beta \to \alpha$ where $\alpha$ is a complete lattice, and for any element $b \in \beta$, the supremum of $f$ over the singleton set $\{b\}$ is equal to $f(b)$. In symbols: \[ \bigsqcup_{x \in \{b\}} f(x) = f(b). \]

iInf_singleton theorem

{f : β → α} {b : β} : ⨅ x ∈ (singleton b : Set β), f x = f b

Full source

theorem iInf_singleton {f : β → α} {b : β} : ⨅ x ∈ (singleton b : Set β), f x = f b := by simp

Infimum over a Singleton Set: $\bigsqcap_{x \in \{b\}} f(x) = f(b)$

Informal description

For any function $f \colon \beta \to \alpha$ where $\alpha$ is a complete lattice, and for any element $b \in \beta$, the infimum of $f$ over the singleton set $\{b\}$ is equal to $f(b)$. In symbols: \[ \bigsqcap_{x \in \{b\}} f(x) = f(b). \]

iSup_pair theorem

{f : β → α} {a b : β} : ⨆ x ∈ ({ a, b } : Set β), f x = f a ⊔ f b

Full source

theorem iSup_pair {f : β → α} {a b : β} : ⨆ x ∈ ({a, b} : Set β), f x = f a ⊔ f b := by
  rw [iSup_insert, iSup_singleton]

Supremum over a Pair Set: $\bigsqcup_{x \in \{a, b\}} f(x) = f(a) \sqcup f(b)$

Informal description

For any function $f \colon \beta \to \alpha$ where $\alpha$ is a complete lattice, and for any elements $a, b \in \beta$, the supremum of $f$ over the pair set $\{a, b\}$ is equal to the join of $f(a)$ and $f(b)$. In symbols: \[ \bigsqcup_{x \in \{a, b\}} f(x) = f(a) \sqcup f(b). \]

iInf_pair theorem

{f : β → α} {a b : β} : ⨅ x ∈ ({ a, b } : Set β), f x = f a ⊓ f b

Full source

theorem iInf_pair {f : β → α} {a b : β} : ⨅ x ∈ ({a, b} : Set β), f x = f a ⊓ f b := by
  rw [iInf_insert, iInf_singleton]

Infimum over a Pair Set: $\bigsqcap_{\{a, b\}} f = f(a) \sqcap f(b)$

Informal description

For any function $f \colon \beta \to \alpha$ where $\alpha$ is a complete lattice, and for any elements $a, b \in \beta$, the infimum of $f$ over the pair set $\{a, b\}$ is equal to the meet of $f(a)$ and $f(b)$. In symbols: \[ \bigsqcap_{x \in \{a, b\}} f(x) = f(a) \sqcap f(b). \]

iSup_image theorem

{γ} {f : β → γ} {g : γ → α} {t : Set β} : ⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b)

Full source

theorem iSup_image {γ} {f : β → γ} {g : γ → α} {t : Set β} :
    ⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b) := by
  rw [← sSup_image, ← sSup_image, ← image_comp, comp_def]

Supremum of Image Equals Supremum of Composition

Informal description

For any set $t \subseteq \beta$, any function $f \colon \beta \to \gamma$, and any function $g \colon \gamma \to \alpha$, the supremum of $g$ over the image of $t$ under $f$ is equal to the supremum of $g \circ f$ over $t$. In symbols: $$\bigsqcup_{c \in f(t)} g(c) = \bigsqcup_{b \in t} g(f(b)).$$

iInf_image theorem

: ∀ {γ} {f : β → γ} {g : γ → α} {t : Set β}, ⨅ c ∈ f '' t, g c = ⨅ b ∈ t, g (f b)

Full source

theorem iInf_image :
    ∀ {γ} {f : β → γ} {g : γ → α} {t : Set β}, ⨅ c ∈ f '' t, g c = ⨅ b ∈ t, g (f b) :=
  @iSup_image αᵒᵈ _ _

Infimum of Image Equals Infimum of Composition

Informal description

For any set $t \subseteq \beta$, any function $f \colon \beta \to \gamma$, and any function $g \colon \gamma \to \alpha$, the infimum of $g$ over the image of $t$ under $f$ is equal to the infimum of $g \circ f$ over $t$. In symbols: $$\bigsqcap_{c \in f(t)} g(c) = \bigsqcap_{b \in t} g(f(b)).$$

iSup_extend_bot theorem

{e : ι → β} (he : Injective e) (f : ι → α) : ⨆ j, extend e f ⊥ j = ⨆ i, f i

Full source

theorem iSup_extend_bot {e : ι → β} (he : Injective e) (f : ι → α) :
    ⨆ j, extend e f ⊥ j = ⨆ i, f i := by
  rw [iSup_split _ fun j => ∃ i, e i = j]
  simp +contextual [he.extend_apply, extend_apply', @iSup_comm _ β ι]

Supremum Equality for Extended Function with Bottom Default: $\bigsqcup_j \text{extend}\,e\,f\,\bot\,j = \bigsqcup_i f(i)$

Informal description

Let $e : \iota \to \beta$ be an injective function and $f : \iota \to \alpha$ be any function into a complete lattice $\alpha$. Then the supremum of the extended function $\text{extend}\,e\,f\,\bot$ over $\beta$ equals the supremum of $f$ over $\iota$, i.e., \[ \bigsqcup_{j \in \beta} \text{extend}\,e\,f\,\bot\,j = \bigsqcup_{i \in \iota} f(i). \] Here, $\text{extend}\,e\,f\,\bot$ is defined as: - $\text{extend}\,e\,f\,\bot\,(e(i)) = f(i)$ for $i \in \iota$ (since $e$ is injective), - $\text{extend}\,e\,f\,\bot\,j = \bot$ for $j \notin \text{range}(e)$.

iInf_extend_top theorem

{e : ι → β} (he : Injective e) (f : ι → α) : ⨅ j, extend e f ⊤ j = iInf f

Full source

theorem iInf_extend_top {e : ι → β} (he : Injective e) (f : ι → α) :
    ⨅ j, extend e f ⊤ j = iInf f :=
  @iSup_extend_bot αᵒᵈ _ _ _ _ he _

Infimum Equality for Extended Function with Top Default: $\bigsqcap_j \text{extend}\,e\,f\,\top\,j = \bigsqcap_i f(i)$

Informal description

Let $e : \iota \to \beta$ be an injective function and $f : \iota \to \alpha$ be any function into a complete lattice $\alpha$. Then the infimum of the extended function $\text{extend}\,e\,f\,\top$ over $\beta$ equals the infimum of $f$ over $\iota$, i.e., \[ \bigsqcap_{j \in \beta} \text{extend}\,e\,f\,\top\,j = \bigsqcap_{i \in \iota} f(i). \] Here, $\text{extend}\,e\,f\,\top$ is defined as: - $\text{extend}\,e\,f\,\top\,(e(i)) = f(i)$ for $i \in \iota$ (since $e$ is injective), - $\text{extend}\,e\,f\,\top\,j = \top$ for $j \notin \text{range}(e)$.

biSup_le_eq_sup theorem

: (⨆ j ≤ i, f j) = (⨆ j < i, f j) ⊔ f i

Full source

theorem biSup_le_eq_sup : (⨆ j ≤ i, f j) = (⨆ j < i, f j) ⊔ f i := by
  rw [iSup_split_single _ i]
  -- Squeezed for a ~10x speedup, though it's still reasonably fast unsqueezed.
  simp only [le_refl, iSup_pos, iSup_and', lt_iff_le_and_ne, and_comm, sup_comm]

Supremum Decomposition for Bounded Indices: $\bigsqcup_{j \leq i} f(j) = (\bigsqcup_{j < i} f(j)) \sqcup f(i)$

Informal description

For any function $f$ mapping into a complete lattice and any index $i$, the supremum of $f(j)$ over all $j \leq i$ equals the join of the supremum of $f(j)$ over all $j < i$ with $f(i)$. That is, \[ \bigsqcup_{j \leq i} f(j) = \left(\bigsqcup_{j < i} f(j)\right) \sqcup f(i). \]

biInf_le_eq_inf theorem

: (⨅ j ≤ i, f j) = (⨅ j < i, f j) ⊓ f i

Full source

theorem biInf_le_eq_inf : (⨅ j ≤ i, f j) = (⨅ j < i, f j) ⊓ f i :=
  biSup_le_eq_sup (α := αᵒᵈ) f i

Infimum Decomposition for Bounded Indices: $\bigsqcap_{j \leq i} f(j) = (\bigsqcap_{j < i} f(j)) \sqcap f(i)$

Informal description

For any function $f$ mapping into a complete lattice and any index $i$, the infimum of $f(j)$ over all $j \leq i$ equals the meet of the infimum of $f(j)$ over all $j < i$ with $f(i)$. That is, \[ \bigsqcap_{j \leq i} f(j) = \left(\bigsqcap_{j < i} f(j)\right) \sqcap f(i). \]

biSup_ge_eq_sup theorem

: (⨆ j ≥ i, f j) = f i ⊔ (⨆ j > i, f j)

Full source

theorem biSup_ge_eq_sup : (⨆ j ≥ i, f j) = f i ⊔ (⨆ j > i, f j) := by
  rw [iSup_split_single _ i]
  -- Squeezed for a ~10x speedup, though it's still reasonably fast unsqueezed.
  simp only [ge_iff_le, le_refl, iSup_pos, ne_comm, iSup_and', gt_iff_lt, lt_iff_le_and_ne,
    and_comm]

Supremum Splitting at Index $i$: $\bigsqcup_{j \geq i} f(j) = f(i) \sqcup \bigsqcup_{j > i} f(j)$

Informal description

For any function $f$ and any index $i$, the supremum of $f(j)$ over all indices $j \geq i$ equals the join of $f(i)$ with the supremum of $f(j)$ over all indices $j > i$. That is, \[ \bigsqcup_{j \geq i} f(j) = f(i) \sqcup \left(\bigsqcup_{j > i} f(j)\right). \]

biInf_ge_eq_inf theorem

: (⨅ j ≥ i, f j) = f i ⊓ (⨅ j > i, f j)

Full source

theorem biInf_ge_eq_inf : (⨅ j ≥ i, f j) = f i ⊓ (⨅ j > i, f j) :=
  biSup_ge_eq_sup (α := αᵒᵈ) f i

Infimum Splitting at Index $i$: $\bigsqcap_{j \geq i} f(j) = f(i) \sqcap \bigsqcap_{j > i} f(j)$

Informal description

For any function $f$ and any index $i$, the infimum of $f(j)$ over all indices $j \geq i$ equals the meet of $f(i)$ with the infimum of $f(j)$ over all indices $j > i$. That is, \[ \bigsqcap_{j \geq i} f(j) = f(i) \sqcap \left(\bigsqcap_{j > i} f(j)\right). \]

iSup_of_empty' theorem

{α ι} [SupSet α] [IsEmpty ι] (f : ι → α) : iSup f = sSup (∅ : Set α)

Full source

theorem iSup_of_empty' {α ι} [SupSet α] [IsEmpty ι] (f : ι → α) : iSup f = sSup (∅ : Set α) :=
  congr_arg sSup (range_eq_empty f)

Supremum of Empty Indexed Family Equals Supremum of Empty Set

Informal description

For any type $\alpha$ with a supremum operator and any empty type $\iota$, the supremum of an indexed family $f : \iota \to \alpha$ is equal to the supremum of the empty set in $\alpha$, i.e., $\bigsqcup_{i \in \iota} f(i) = \mathrm{sSup}(\emptyset)$.

iInf_of_isEmpty theorem

{α ι} [InfSet α] [IsEmpty ι] (f : ι → α) : iInf f = sInf (∅ : Set α)

Full source

theorem iInf_of_isEmpty {α ι} [InfSet α] [IsEmpty ι] (f : ι → α) : iInf f = sInf (∅ : Set α) :=
  congr_arg sInf (range_eq_empty f)

Indexed Infimum over Empty Domain Equals Infimum of Empty Set

Informal description

For any type $\alpha$ equipped with an infimum structure and any empty type $\iota$, the indexed infimum $\bigsqcap_{i \in \iota} f(i)$ of a function $f : \iota \to \alpha$ is equal to the infimum of the empty set in $\alpha$, i.e., $\bigsqcap_{i \in \iota} f(i) = \mathrm{sInf}(\emptyset)$.

iSup_of_empty theorem

[IsEmpty ι] (f : ι → α) : iSup f = ⊥

Full source

theorem iSup_of_empty [IsEmpty ι] (f : ι → α) : iSup f = ⊥ :=
  (iSup_of_empty' f).trans sSup_empty

Supremum of Empty Indexed Family is Bottom Element

Informal description

For any complete lattice $\alpha$ and any empty type $\iota$, the supremum of an indexed family $f : \iota \to \alpha$ is equal to the bottom element $\bot$ of $\alpha$, i.e., \[ \bigsqcup_{i \in \iota} f(i) = \bot. \]

iInf_of_empty theorem

[IsEmpty ι] (f : ι → α) : iInf f = ⊤

Full source

theorem iInf_of_empty [IsEmpty ι] (f : ι → α) : iInf f = ⊤ :=
  @iSup_of_empty αᵒᵈ _ _ _ f

Infimum of Empty Indexed Family is Top Element

Informal description

For any complete lattice $\alpha$ and any empty type $\iota$, the infimum of an indexed family $f : \iota \to \alpha$ is equal to the top element $\top$ of $\alpha$, i.e., \[ \bigsqcap_{i \in \iota} f(i) = \top. \]

isGLB_biInf theorem

{s : Set β} {f : β → α} : IsGLB (f '' s) (⨅ x ∈ s, f x)

Full source

theorem isGLB_biInf {s : Set β} {f : β → α} : IsGLB (f '' s) (⨅ x ∈ s, f x) := by
  simpa only [range_comp, Subtype.range_coe, iInf_subtype'] using
    @isGLB_iInf α s _ (f ∘ fun x => (x : β))

Bounded Infimum is Greatest Lower Bound of Image

Informal description

For any set $s$ in a type $\beta$ and any function $f : \beta \to \alpha$ where $\alpha$ is a complete lattice, the bounded infimum $\bigsqcap_{x \in s} f(x)$ is the greatest lower bound of the image of $s$ under $f$. That is, $\bigsqcap_{x \in s} f(x)$ is a lower bound for $\{f(x) \mid x \in s\}$ and is greater than or equal to any other lower bound of this set.

isLUB_biSup theorem

{s : Set β} {f : β → α} : IsLUB (f '' s) (⨆ x ∈ s, f x)

Full source

theorem isLUB_biSup {s : Set β} {f : β → α} : IsLUB (f '' s) (⨆ x ∈ s, f x) := by
  simpa only [range_comp, Subtype.range_coe, iSup_subtype'] using
    @isLUB_iSup α s _ (f ∘ fun x => (x : β))

Bounded Supremum is Least Upper Bound of Image

Informal description

For any set $s$ in a type $\beta$ and any function $f : \beta \to \alpha$ where $\alpha$ is a complete lattice, the bounded supremum $\bigsqcup_{x \in s} f(x)$ is the least upper bound of the image of $s$ under $f$. That is, $\bigsqcup_{x \in s} f(x)$ is an upper bound for $\{f(x) \mid x \in s\}$ and is less than or equal to any other upper bound of this set.

iSup_sigma theorem

{p : β → Type*} {f : Sigma p → α} : ⨆ x, f x = ⨆ (i) (j), f ⟨i, j⟩

Full source

theorem iSup_sigma {p : β → Type*} {f : Sigma p → α} : ⨆ x, f x = ⨆ (i) (j), f ⟨i, j⟩ :=
  eq_of_forall_ge_iff fun c => by simp only [iSup_le_iff, Sigma.forall]

Supremum over Dependent Pair Equals Iterated Supremum

Informal description

For any indexed family of types $p : \beta \to \text{Type}$ and any function $f : \Sigma p \to \alpha$ (where $\Sigma p$ is the dependent sum type), the supremum of $f$ over all pairs $(i, j)$ is equal to the supremum of $f$ over all elements of $\Sigma p$. In other words, \[ \bigsqcup_{x \in \Sigma p} f(x) = \bigsqcup_{i \in \beta} \bigsqcup_{j \in p(i)} f(\langle i, j \rangle). \]

iInf_sigma theorem

{p : β → Type*} {f : Sigma p → α} : ⨅ x, f x = ⨅ (i) (j), f ⟨i, j⟩

Full source

theorem iInf_sigma {p : β → Type*} {f : Sigma p → α} : ⨅ x, f x = ⨅ (i) (j), f ⟨i, j⟩ :=
  @iSup_sigma αᵒᵈ _ _ _ _

Infimum over Dependent Pair Equals Iterated Infimum

Informal description

For any indexed family of types $p : \beta \to \text{Type}$ and any function $f : \Sigma p \to \alpha$ (where $\Sigma p$ is the dependent sum type), the infimum of $f$ over all pairs $(i, j)$ is equal to the infimum of $f$ over all elements of $\Sigma p$. In other words, \[ \bigsqcap_{x \in \Sigma p} f(x) = \bigsqcap_{i \in \beta} \bigsqcap_{j \in p(i)} f(\langle i, j \rangle). \]

iSup_sigma' theorem

{κ : β → Type*} (f : ∀ i, κ i → α) : (⨆ i, ⨆ j, f i j) = ⨆ x : Σ i, κ i, f x.1 x.2

Full source

lemma iSup_sigma' {κ : β → Type*} (f : ∀ i, κ i → α) :
    (⨆ i, ⨆ j, f i j) = ⨆ x : Σ i, κ i, f x.1 x.2 := (iSup_sigma (f := fun x ↦ f x.1 x.2)).symm

Iterated Supremum Equals Supremum over Dependent Pairs

Informal description

For any indexed family of types $\kappa : \beta \to \text{Type}$ and any function $f : \forall i, \kappa i \to \alpha$, the iterated supremum $\bigsqcup_i \bigsqcup_j f(i, j)$ is equal to the supremum of $f$ over all dependent pairs $(x : \Sigma i, \kappa i)$, i.e., \[ \bigsqcup_i \bigsqcup_j f(i, j) = \bigsqcup_{x : \Sigma i, \kappa i} f(x.1, x.2). \]

iInf_sigma' theorem

{κ : β → Type*} (f : ∀ i, κ i → α) : (⨅ i, ⨅ j, f i j) = ⨅ x : Σ i, κ i, f x.1 x.2

Full source

lemma iInf_sigma' {κ : β → Type*} (f : ∀ i, κ i → α) :
    (⨅ i, ⨅ j, f i j) = ⨅ x : Σ i, κ i, f x.1 x.2 := (iInf_sigma (f := fun x ↦ f x.1 x.2)).symm

Iterated Infimum Equals Infimum over Dependent Pairs

Informal description

For any indexed family of types $\kappa : \beta \to \text{Type}$ and any function $f : \forall i, \kappa i \to \alpha$ where $\alpha$ is a complete lattice, the iterated infimum $\bigsqcap_i \bigsqcap_j f(i, j)$ is equal to the infimum of $f$ over all dependent pairs $(x : \Sigma i, \kappa i)$. That is, \[ \bigsqcap_i \bigsqcap_j f(i, j) = \bigsqcap_{x : \Sigma i, \kappa i} f(x.1, x.2). \]

iSup_psigma theorem

{ι : Sort*} {κ : ι → Sort*} (f : (Σ' i, κ i) → α) : ⨆ ij, f ij = ⨆ i, ⨆ j, f ⟨i, j⟩

Full source

lemma iSup_psigma {ι : Sort*} {κ : ι → Sort*} (f : (Σ' i, κ i) → α) :
    ⨆ ij, f ij = ⨆ i, ⨆ j, f ⟨i, j⟩ :=
  eq_of_forall_ge_iff fun c ↦ by simp only [iSup_le_iff, PSigma.forall]

Supremum Decomposition for Dependent Pairs

Informal description

Let $\alpha$ be a complete lattice, $\iota$ be a sort, and $\kappa : \iota \to \Sort$ be a family of sorts. For any function $f : (\Sigma' i, \kappa i) \to \alpha$, the supremum of $f$ over all pairs $(i, j)$ is equal to the iterated supremum where we first take the supremum over $j$ for each fixed $i$, and then take the supremum over $i$. In symbols: \[ \bigsqcup_{ij} f(ij) = \bigsqcup_i \bigsqcup_j f(i, j) \]

iInf_psigma theorem

{ι : Sort*} {κ : ι → Sort*} (f : (Σ' i, κ i) → α) : ⨅ ij, f ij = ⨅ i, ⨅ j, f ⟨i, j⟩

Full source

lemma iInf_psigma {ι : Sort*} {κ : ι → Sort*} (f : (Σ' i, κ i) → α) :
    ⨅ ij, f ij = ⨅ i, ⨅ j, f ⟨i, j⟩ :=
  eq_of_forall_le_iff fun c ↦ by simp only [le_iInf_iff, PSigma.forall]

Infimum over Sigma Type Equals Iterated Infimum

Informal description

For any indexed family of types $\kappa : \iota \to \text{Sort}^*$ and any function $f : (\Sigma' i, \kappa i) \to \alpha$ where $\alpha$ is a complete lattice, the infimum over all pairs $(i, j)$ is equal to the iterated infimum over $i$ and then $j$. That is, \[ \bigsqcap_{ij} f(ij) = \bigsqcap_i \bigsqcap_j f\langle i, j \rangle. \]

iSup_psigma' theorem

{ι : Sort*} {κ : ι → Sort*} (f : ∀ i, κ i → α) : (⨆ i, ⨆ j, f i j) = ⨆ ij : Σ' i, κ i, f ij.1 ij.2

Full source

lemma iSup_psigma' {ι : Sort*} {κ : ι → Sort*} (f : ∀ i, κ i → α) :
    (⨆ i, ⨆ j, f i j) = ⨆ ij : Σ' i, κ i, f ij.1 ij.2 := (iSup_psigma fun x ↦ f x.1 x.2).symm

Iterated Supremum Equals Supremum over Dependent Pairs

Informal description

Let $\alpha$ be a complete lattice, $\iota$ be a sort, and $\kappa : \iota \to \text{Sort}$ be a family of sorts. For any function $f : \forall i, \kappa i \to \alpha$, the iterated supremum $\bigsqcup_i \bigsqcup_j f(i, j)$ is equal to the supremum over all dependent pairs $(i, j) \in \Sigma' i, \kappa i$ of $f(i, j)$. In symbols: \[ \bigsqcup_i \bigsqcup_j f(i, j) = \bigsqcup_{(i,j)} f(i, j) \]

iInf_psigma' theorem

{ι : Sort*} {κ : ι → Sort*} (f : ∀ i, κ i → α) : (⨅ i, ⨅ j, f i j) = ⨅ ij : Σ' i, κ i, f ij.1 ij.2

Full source

lemma iInf_psigma' {ι : Sort*} {κ : ι → Sort*} (f : ∀ i, κ i → α) :
    (⨅ i, ⨅ j, f i j) = ⨅ ij : Σ' i, κ i, f ij.1 ij.2 := (iInf_psigma fun x ↦ f x.1 x.2).symm

Iterated Infimum Equals Sigma-Type Infimum

Informal description

For any indexed family of types $\kappa : \iota \to \text{Sort}^*$ and any function $f : \forall i, \kappa i \to \alpha$ where $\alpha$ is a complete lattice, the iterated infimum over $i$ and $j$ of $f i j$ is equal to the infimum over all pairs $(i, j)$ in the sigma type $\Sigma' i, \kappa i$. That is, \[ \bigsqcap_i \bigsqcap_j f i j = \bigsqcap_{(i,j)} f i j. \]

iSup_prod theorem

{f : β × γ → α} : ⨆ x, f x = ⨆ (i) (j), f (i, j)

Full source

theorem iSup_prod {f : β × γ → α} : ⨆ x, f x = ⨆ (i) (j), f (i, j) :=
  eq_of_forall_ge_iff fun c => by simp only [iSup_le_iff, Prod.forall]

Supremum over Product Equals Iterated Supremum

Informal description

For any function $f : \beta \times \gamma \to \alpha$ from the product of types $\beta$ and $\gamma$ to a complete lattice $\alpha$, the supremum of $f$ over all pairs $(i,j) \in \beta \times \gamma$ is equal to the iterated supremum where we first take the supremum over $i \in \beta$ and then over $j \in \gamma$ of $f(i,j)$. In symbols: \[ \bigsqcup_{x \in \beta \times \gamma} f(x) = \bigsqcup_{i \in \beta} \bigsqcup_{j \in \gamma} f(i,j) \]

iInf_prod theorem

{f : β × γ → α} : ⨅ x, f x = ⨅ (i) (j), f (i, j)

Full source

theorem iInf_prod {f : β × γ → α} : ⨅ x, f x = ⨅ (i) (j), f (i, j) :=
  @iSup_prod αᵒᵈ _ _ _ _

Infimum over Product Equals Iterated Infimum

Informal description

For any function $f \colon \beta \times \gamma \to \alpha$ where $\alpha$ is a complete lattice, the infimum of $f$ over the product $\beta \times \gamma$ equals the iterated infimum over $\beta$ and $\gamma$. That is, \[ \bigsqcap_{x \in \beta \times \gamma} f(x) = \bigsqcap_{i \in \beta} \bigsqcap_{j \in \gamma} f(i,j). \]

iSup_prod' theorem

(f : β → γ → α) : (⨆ i, ⨆ j, f i j) = ⨆ x : β × γ, f x.1 x.2

Full source

lemma iSup_prod' (f : β → γ → α) : (⨆ i, ⨆ j, f i j) = ⨆ x : β × γ, f x.1 x.2 :=
(iSup_prod (f := fun x ↦ f x.1 x.2)).symm

Iterated Supremum Equals Supremum over Product

Informal description

For any function $f : \beta \to \gamma \to \alpha$ where $\alpha$ is a complete lattice, the iterated supremum $\bigsqcup_{i \in \beta} \bigsqcup_{j \in \gamma} f(i,j)$ is equal to the supremum $\bigsqcup_{x \in \beta \times \gamma} f(x.1, x.2)$ taken over all pairs $x = (i,j)$ in the product type $\beta \times \gamma$.

iInf_prod' theorem

(f : β → γ → α) : (⨅ i, ⨅ j, f i j) = ⨅ x : β × γ, f x.1 x.2

Full source

lemma iInf_prod' (f : β → γ → α) : (⨅ i, ⨅ j, f i j) = ⨅ x : β × γ, f x.1 x.2 :=
(iInf_prod (f := fun x ↦ f x.1 x.2)).symm

Iterated Infimum Equals Infimum over Product

Informal description

For any function $f \colon \beta \to \gamma \to \alpha$ where $\alpha$ is a complete lattice, the iterated infimum $\bigsqcap_{i \in \beta} \bigsqcap_{j \in \gamma} f(i,j)$ is equal to the infimum $\bigsqcap_{x \in \beta \times \gamma} f(x.1, x.2)$ taken over all pairs $x = (i,j)$ in the product type $\beta \times \gamma$.

biSup_prod theorem

{f : β × γ → α} {s : Set β} {t : Set γ} : ⨆ x ∈ s ×ˢ t, f x = ⨆ (a ∈ s) (b ∈ t), f (a, b)

Full source

theorem biSup_prod {f : β × γ → α} {s : Set β} {t : Set γ} :
    ⨆ x ∈ s ×ˢ t, f x = ⨆ (a ∈ s) (b ∈ t), f (a, b) := by
  simp_rw [iSup_prod, mem_prod, iSup_and]
  exact iSup_congr fun _ => iSup_comm

Supremum over Cartesian Product Equals Iterated Supremum

Informal description

For any function $f : \beta \times \gamma \to \alpha$ where $\alpha$ is a complete lattice, and any subsets $s \subseteq \beta$ and $t \subseteq \gamma$, the supremum of $f$ over the Cartesian product $s \times t$ is equal to the iterated supremum where we first take the supremum over $a \in s$ and then over $b \in t$ of $f(a,b)$. In symbols: \[ \bigsqcup_{x \in s \times t} f(x) = \bigsqcup_{a \in s} \bigsqcup_{b \in t} f(a,b) \]

biInf_prod theorem

{f : β × γ → α} {s : Set β} {t : Set γ} : ⨅ x ∈ s ×ˢ t, f x = ⨅ (a ∈ s) (b ∈ t), f (a, b)

Full source

theorem biInf_prod {f : β × γ → α} {s : Set β} {t : Set γ} :
    ⨅ x ∈ s ×ˢ t, f x = ⨅ (a ∈ s) (b ∈ t), f (a, b) :=
  @biSup_prod αᵒᵈ _ _ _ _ _ _

Infimum over Cartesian Product Equals Iterated Infimum

Informal description

For any function $f \colon \beta \times \gamma \to \alpha$ where $\alpha$ is a complete lattice, and any subsets $s \subseteq \beta$ and $t \subseteq \gamma$, the infimum of $f$ over the Cartesian product $s \times t$ is equal to the iterated infimum where we first take the infimum over $a \in s$ and then over $b \in t$ of $f(a,b)$. In symbols: \[ \bigsqcap_{x \in s \times t} f(x) = \bigsqcap_{a \in s} \bigsqcap_{b \in t} f(a,b) \]

iSup_image2 theorem

 {γ δ} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) : ⨆ d ∈ image2 f s t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c)

Full source

theorem iSup_image2 {γ δ} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) :
    ⨆ d ∈ image2 f s t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c) := by
  rw [← image_prod, iSup_image, biSup_prod]

Supremum of Binary Image Equals Iterated Supremum

Informal description

For any complete lattice $\alpha$, any sets $s \subseteq \beta$ and $t \subseteq \gamma$, and any functions $f \colon \beta \to \gamma \to \delta$ and $g \colon \delta \to \alpha$, the supremum of $g$ over the image of $f$ applied to $s$ and $t$ equals the iterated supremum of $g \circ f$ over $s$ and $t$. In symbols: \[ \bigsqcup_{d \in \text{image2}(f,s,t)} g(d) = \bigsqcup_{b \in s} \bigsqcup_{c \in t} g(f(b,c)) \]

iInf_image2 theorem

 {γ δ} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) : ⨅ d ∈ image2 f s t, g d = ⨅ b ∈ s, ⨅ c ∈ t, g (f b c)

Full source

theorem iInf_image2 {γ δ} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) :
    ⨅ d ∈ image2 f s t, g d = ⨅ b ∈ s, ⨅ c ∈ t, g (f b c) :=
  iSup_image2 f s t (toDualtoDual ∘ g)

Infimum of Binary Image Equals Iterated Infimum

Informal description

For any complete lattice $\alpha$, any sets $s \subseteq \beta$ and $t \subseteq \gamma$, and any functions $f \colon \beta \to \gamma \to \delta$ and $g \colon \delta \to \alpha$, the infimum of $g$ over the image of $f$ applied to $s$ and $t$ equals the iterated infimum of $g \circ f$ over $s$ and $t$. In symbols: \[ \bigsqcap_{d \in \text{image2}(f,s,t)} g(d) = \bigsqcap_{b \in s} \bigsqcap_{c \in t} g(f(b,c)) \]

iSup_sum theorem

{f : β ⊕ γ → α} : ⨆ x, f x = (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j)

Full source

theorem iSup_sum {f : β ⊕ γ → α} : ⨆ x, f x = (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j) :=
  eq_of_forall_ge_iff fun c => by simp only [sup_le_iff, iSup_le_iff, Sum.forall]

Supremum over Sum Type Decomposes into Suprema over Components

Informal description

For any function $f : \beta \oplus \gamma \to \alpha$ from a sum type to a complete lattice $\alpha$, the supremum of $f$ over all inputs is equal to the supremum of $f$ over left injections $\sqcup$ the supremum of $f$ over right injections. In other words: \[ \bigsqcup_{x \in \beta \oplus \gamma} f(x) = \left(\bigsqcup_{i \in \beta} f(\mathrm{inl}(i))\right) \sqcup \left(\bigsqcup_{j \in \gamma} f(\mathrm{inr}(j))\right) \]

iInf_sum theorem

{f : β ⊕ γ → α} : ⨅ x, f x = (⨅ i, f (Sum.inl i)) ⊓ ⨅ j, f (Sum.inr j)

Full source

theorem iInf_sum {f : β ⊕ γ → α} : ⨅ x, f x = (⨅ i, f (Sum.inl i)) ⊓ ⨅ j, f (Sum.inr j) :=
  @iSup_sum αᵒᵈ _ _ _ _

Infimum Decomposition for Sum Type: $\bigsqcap f(x) = \bigsqcap_i f(\mathrm{inl}(i)) \sqcap \bigsqcap_j f(\mathrm{inr}(j))$

Informal description

For any function $f : \beta \oplus \gamma \to \alpha$ from a sum type to a complete lattice $\alpha$, the infimum of $f$ over all inputs is equal to the infimum of $f$ over left injections $\sqcap$ the infimum of $f$ over right injections. In other words: \[ \bigsqcap_{x \in \beta \oplus \gamma} f(x) = \left(\bigsqcap_{i \in \beta} f(\mathrm{inl}(i))\right) \sqcap \left(\bigsqcap_{j \in \gamma} f(\mathrm{inr}(j))\right) \]

iSup_option theorem

(f : Option β → α) : ⨆ o, f o = f none ⊔ ⨆ b, f (Option.some b)

Full source

theorem iSup_option (f : Option β → α) : ⨆ o, f o = f none ⊔ ⨆ b, f (Option.some b) :=
  eq_of_forall_ge_iff fun c => by simp only [iSup_le_iff, sup_le_iff, Option.forall]

Supremum Decomposition for Option Type: $\bigsqcup f(o) = f(\text{none}) \sqcup \bigsqcup_b f(\text{some}\,b)$

Informal description

For any function $f : \text{Option}\,\beta \to \alpha$ from the option type over $\beta$ to a complete lattice $\alpha$, the supremum of $f$ over all options is equal to the supremum of $f(\text{none})$ and the supremum of $f$ over all $\text{some}\,b$ for $b \in \beta$. That is, \[ \bigsqcup_{o \in \text{Option}\,\beta} f(o) = f(\text{none}) \sqcup \bigsqcup_{b \in \beta} f(\text{some}\,b). \]

iInf_option theorem

(f : Option β → α) : ⨅ o, f o = f none ⊓ ⨅ b, f (Option.some b)

Full source

theorem iInf_option (f : Option β → α) : ⨅ o, f o = f none ⊓ ⨅ b, f (Option.some b) :=
  @iSup_option αᵒᵈ _ _ _

Infimum Decomposition for Option Type: $\bigsqcap f(o) = f(\text{none}) \sqcap \bigsqcap_b f(\text{some}\,b)$

Informal description

For any function $f : \text{Option}\,\beta \to \alpha$ from the option type over $\beta$ to a complete lattice $\alpha$, the infimum of $f$ over all options is equal to the infimum of $f(\text{none})$ and the infimum of $f$ over all $\text{some}\,b$ for $b \in \beta$. That is, \[ \bigsqcap_{o \in \text{Option}\,\beta} f(o) = f(\text{none}) \sqcap \bigsqcap_{b \in \beta} f(\text{some}\,b). \]

iSup_option_elim theorem

(a : α) (f : β → α) : ⨆ o : Option β, o.elim a f = a ⊔ ⨆ b, f b

Full source

/-- A version of `iSup_option` useful for rewriting right-to-left. -/
theorem iSup_option_elim (a : α) (f : β → α) : ⨆ o : Option β, o.elim a f = a ⊔ ⨆ b, f b := by
  simp [iSup_option]

Supremum Decomposition for Option Elimination: $\bigsqcup o.\text{elim}\,a\,f = a \sqcup \bigsqcup_b f(b)$

Informal description

For any element $a$ in a complete lattice $\alpha$ and any function $f : \beta \to \alpha$, the supremum of the function $o \mapsto o.\text{elim}\,a\,f$ over all options $o \in \text{Option}\,\beta$ is equal to the supremum of $a$ and the supremum of $f$ over all $b \in \beta$. That is, \[ \bigsqcup_{o \in \text{Option}\,\beta} o.\text{elim}\,a\,f = a \sqcup \bigsqcup_{b \in \beta} f(b). \]

iInf_option_elim theorem

(a : α) (f : β → α) : ⨅ o : Option β, o.elim a f = a ⊓ ⨅ b, f b

Full source

/-- A version of `iInf_option` useful for rewriting right-to-left. -/
theorem iInf_option_elim (a : α) (f : β → α) : ⨅ o : Option β, o.elim a f = a ⊓ ⨅ b, f b :=
  @iSup_option_elim αᵒᵈ _ _ _ _

Infimum Decomposition for Option Elimination: $\bigsqcap o.\text{elim}\,a\,f = a \sqcap \bigsqcap_b f(b)$

Informal description

For any element $a$ in a complete lattice $\alpha$ and any function $f : \beta \to \alpha$, the infimum of the function $o \mapsto o.\text{elim}\,a\,f$ over all options $o \in \text{Option}\,\beta$ is equal to the infimum of $a$ and the infimum of $f$ over all $b \in \beta$. That is, \[ \bigsqcap_{o \in \text{Option}\,\beta} o.\text{elim}\,a\,f = a \sqcap \bigsqcap_{b \in \beta} f(b). \]

iSup_ne_bot_subtype theorem

(f : ι → α) : ⨆ i : { i // f i ≠ ⊥ }, f i = ⨆ i, f i

Full source

/-- When taking the supremum of `f : ι → α`, the elements of `ι` on which `f` gives `⊥` can be
dropped, without changing the result. -/
@[simp]
theorem iSup_ne_bot_subtype (f : ι → α) : ⨆ i : { i // f i ≠ ⊥ }, f i = ⨆ i, f i := by
  by_cases htriv : ∀ i, f i = ⊥
  · simp only [iSup_bot, (funext htriv : f = _)]
  refine (iSup_comp_le f _).antisymm (iSup_mono' fun i => ?_)
  by_cases hi : f i = ⊥
  · rw [hi]
    obtain ⟨i₀, hi₀⟩ := not_forall.mp htriv
    exact ⟨⟨i₀, hi₀⟩, bot_le⟩
  · exact ⟨⟨i, hi⟩, rfl.le⟩

Supremum Unaffected by Bottom Elements: $\bigsqcup_{f(i) \neq \bot} f(i) = \bigsqcup_i f(i)$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$ with a bottom element $\bot$, the supremum of $f$ over all indices $i$ where $f(i) \neq \bot$ is equal to the supremum of $f$ over all indices. That is, \[ \bigsqcup_{i \in \{i \mid f(i) \neq \bot\}} f(i) = \bigsqcup_{i} f(i). \]

iInf_ne_top_subtype theorem

(f : ι → α) : ⨅ i : { i // f i ≠ ⊤ }, f i = ⨅ i, f i

Full source

/-- When taking the infimum of `f : ι → α`, the elements of `ι` on which `f` gives `⊤` can be
dropped, without changing the result. -/
theorem iInf_ne_top_subtype (f : ι → α) : ⨅ i : { i // f i ≠ ⊤ }, f i = ⨅ i, f i :=
  @iSup_ne_bot_subtype αᵒᵈ ι _ f

Infimum Unaffected by Top Elements: $\bigsqcap_{f(i) \neq \top} f(i) = \bigsqcap_i f(i)$

Informal description

For any indexed family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$ with a top element $\top$, the infimum of $f$ over all indices $i$ where $f(i) \neq \top$ is equal to the infimum of $f$ over all indices. That is, \[ \bigsqcap_{i \in \{i \mid f(i) \neq \top\}} f(i) = \bigsqcap_{i} f(i). \]

sSup_image2 theorem

{f : β → γ → α} {s : Set β} {t : Set γ} : sSup (image2 f s t) = ⨆ (a ∈ s) (b ∈ t), f a b

Full source

theorem sSup_image2 {f : β → γ → α} {s : Set β} {t : Set γ} :
    sSup (image2 f s t) = ⨆ (a ∈ s) (b ∈ t), f a b := by rw [← image_prod, sSup_image, biSup_prod]

Supremum of Binary Image Equals Iterated Supremum: $\sup \text{image2}(f,s,t) = \bigsqcup_{a \in s} \bigsqcup_{b \in t} f(a,b)$

Informal description

For any complete lattice $\alpha$, any binary function $f : \beta \to \gamma \to \alpha$, and any subsets $s \subseteq \beta$, $t \subseteq \gamma$, the supremum of the image of $f$ on $s \times t$ equals the iterated supremum of $f(a,b)$ over $a \in s$ and $b \in t$. In symbols: \[ \sup \{f(a,b) \mid a \in s, b \in t\} = \bigsqcup_{a \in s} \bigsqcup_{b \in t} f(a,b) \]

sInf_image2 theorem

{f : β → γ → α} {s : Set β} {t : Set γ} : sInf (image2 f s t) = ⨅ (a ∈ s) (b ∈ t), f a b

Full source

theorem sInf_image2 {f : β → γ → α} {s : Set β} {t : Set γ} :
    sInf (image2 f s t) = ⨅ (a ∈ s) (b ∈ t), f a b := by rw [← image_prod, sInf_image, biInf_prod]

Infimum of Binary Image Equals Iterated Infimum: $\inf \text{image2}(f,s,t) = \bigsqcap_{a \in s} \bigsqcap_{b \in t} f(a,b)$

Informal description

For any complete lattice $\alpha$, any binary function $f \colon \beta \times \gamma \to \alpha$, and any subsets $s \subseteq \beta$ and $t \subseteq \gamma$, the infimum of the image of $f$ on $s \times t$ equals the iterated infimum of $f(a,b)$ over $a \in s$ and $b \in t$. In symbols: \[ \inf \{f(a,b) \mid a \in s, b \in t\} = \bigsqcap_{a \in s} \bigsqcap_{b \in t} f(a,b). \]

iSup_eq_top theorem

(f : ι → α) : iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i

Full source

theorem iSup_eq_top (f : ι → α) : iSupiSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i := by
  simp only [← sSup_range, sSup_eq_top, Set.exists_range_iff]

Supremum Equals Top iff All Elements Below Top are Bounded by Some Function Value

Informal description

For a function $f : \iota \to \alpha$ mapping to a complete linear order $\alpha$, the supremum of the range of $f$ equals the top element $\top$ if and only if for every element $b < \top$, there exists an index $i$ such that $b < f(i)$.

iInf_eq_bot theorem

(f : ι → α) : iInf f = ⊥ ↔ ∀ b > ⊥, ∃ i, f i < b

Full source

theorem iInf_eq_bot (f : ι → α) : iInfiInf f = ⊥ ↔ ∀ b > ⊥, ∃ i, f i < b := by
  simp only [← sInf_range, sInf_eq_bot, Set.exists_range_iff]

Characterization of Infimum Equals Bottom: $\bigsqcap_i f(i) = \bot$

Informal description

For a function $f : \iota \to \alpha$ where $\alpha$ is a complete linear order, the infimum of the range of $f$ equals the bottom element $\bot$ if and only if for every element $b > \bot$ in $\alpha$, there exists an index $i$ such that $f(i) < b$.

iSup₂_eq_top theorem

(f : ∀ i, κ i → α) : ⨆ i, ⨆ j, f i j = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j

Full source

lemma iSup₂_eq_top (f : ∀ i, κ i → α) : ⨆ i, ⨆ j, f i j⨆ i, ⨆ j, f i j = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j := by
  simp_rw [iSup_psigma', iSup_eq_top, PSigma.exists]

Characterization of Iterated Supremum Equals Top: $\bigsqcup_i \bigsqcup_j f(i,j) = \top$

Informal description

Let $\alpha$ be a complete linear order and let $f : \forall i, \kappa i \to \alpha$ be a doubly indexed family of elements in $\alpha$. The iterated supremum $\bigsqcup_i \bigsqcup_j f(i,j)$ equals the top element $\top$ if and only if for every element $b < \top$ in $\alpha$, there exist indices $i$ and $j$ such that $b < f(i,j)$.

iInf₂_eq_bot theorem

(f : ∀ i, κ i → α) : ⨅ i, ⨅ j, f i j = ⊥ ↔ ∀ b > ⊥, ∃ i j, f i j < b

Full source

lemma iInf₂_eq_bot (f : ∀ i, κ i → α) : ⨅ i, ⨅ j, f i j⨅ i, ⨅ j, f i j = ⊥ ↔ ∀ b > ⊥, ∃ i j, f i j < b := by
  simp_rw [iInf_psigma', iInf_eq_bot, PSigma.exists]

Characterization of Double Infimum Equals Bottom: $\bigsqcap_i \bigsqcap_j f(i,j) = \bot$

Informal description

For a complete linear order $\alpha$ and a doubly indexed family of elements $f : \forall i, \kappa i \to \alpha$, the double infimum $\bigsqcap_i \bigsqcap_j f(i, j)$ equals the bottom element $\bot$ if and only if for every element $b > \bot$ in $\alpha$, there exist indices $i$ and $j$ such that $f(i, j) < b$.

Prop.instCompleteLattice instance

: CompleteLattice Prop

Full source

instance Prop.instCompleteLattice : CompleteLattice Prop where
  __ := Prop.instBoundedOrder
  __ := Prop.instDistribLattice
  sSup s := ∃ a ∈ s, a
  le_sSup _ a h p := ⟨a, h, p⟩
  sSup_le _ _ h := fun ⟨b, h', p⟩ => h b h' p
  sInf s := ∀ a, a ∈ s → a
  sInf_le _ a h p := p a h
  le_sInf _ _ h p b hb := h b hb p

Complete Lattice Structure on Propositions

Informal description

The set of propositions forms a complete lattice, where the supremum (join) of a collection of propositions is given by their existential quantification and the infimum (meet) is given by their universal quantification. The top element is `True` and the bottom element is `False`.

Prop.instCompleteLinearOrder instance

: CompleteLinearOrder Prop

Full source

noncomputable instance Prop.instCompleteLinearOrder : CompleteLinearOrder Prop where
  __ := Prop.instCompleteLattice
  __ := Prop.linearOrder
  __ := BooleanAlgebra.toBiheytingAlgebra

Complete Linear Order Structure on Propositions

Informal description

The set of propositions forms a complete linear order, where the order relation is given by implication ($\leq$ corresponds to $\rightarrow$), and the supremum (join) and infimum (meet) operations correspond to existential and universal quantification respectively. This structure combines the properties of a complete lattice with those of a linear order on propositions.

sSup_Prop_eq theorem

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

Full source

@[simp]
theorem sSup_Prop_eq {s : Set Prop} : sSup s = ∃ p ∈ s, p :=
  rfl

Supremum of a Set of Propositions is Existential Quantification

Informal description

For any set $S$ of propositions, the supremum of $S$ is equal to the existential quantification over all propositions in $S$, i.e., $\bigvee S = \exists p \in S, p$.

sInf_Prop_eq theorem

{s : Set Prop} : sInf s = ∀ p ∈ s, p

Full source

@[simp]
theorem sInf_Prop_eq {s : Set Prop} : sInf s = ∀ p ∈ s, p :=
  rfl

Infimum of Proposition Set Equals Universal Quantification

Informal description

For any set $S$ of propositions, the infimum of $S$ is equal to the universal quantification over all propositions in $S$, i.e., $\bigwedge S = \forall p \in S, p$.

iSup_Prop_eq theorem

{p : ι → Prop} : ⨆ i, p i = ∃ i, p i

Full source

@[simp]
theorem iSup_Prop_eq {p : ι → Prop} : ⨆ i, p i = ∃ i, p i :=
  le_antisymm (fun ⟨_, ⟨i, (eq : p i = _)⟩, hq⟩ => ⟨i, eq.symm ▸ hq⟩) fun ⟨i, hi⟩ =>
    ⟨p i, ⟨i, rfl⟩, hi⟩

Supremum of Propositions as Existential Quantification

Informal description

For any indexed family of propositions $(p_i)_{i \in \iota}$, the supremum $\bigsqcup_i p_i$ is equivalent to the existential quantification $\exists i, p_i$.

iInf_Prop_eq theorem

{p : ι → Prop} : ⨅ i, p i = ∀ i, p i

Full source

@[simp]
theorem iInf_Prop_eq {p : ι → Prop} : ⨅ i, p i = ∀ i, p i :=
  le_antisymm (fun h i => h _ ⟨i, rfl⟩) fun h _ ⟨i, Eq⟩ => Eq ▸ h i

Infimum of Propositions as Universal Quantification

Informal description

For any indexed family of propositions $(p_i)_{i \in \iota}$, the infimum $\bigsqcap_i p_i$ is equal to the universal quantification $\forall i, p_i$.

Pi.supSet instance

{α : Type*} {β : α → Type*} [∀ i, SupSet (β i)] : SupSet (∀ i, β i)

Full source

instance Pi.supSet {α : Type*} {β : α → Type*} [∀ i, SupSet (β i)] : SupSet (∀ i, β i) :=
  ⟨fun s i => ⨆ f : s, (f : ∀ i, β i) i⟩

Pointwise Supremum Operator on Product Types

Informal description

For any family of types $\beta : \alpha \to \text{Type}$ where each $\beta_i$ has a supremum operator, the product type $\prod_{i} \beta_i$ inherits a supremum operator defined pointwise. That is, for any set $s$ of functions in $\prod_{i} \beta_i$, the supremum $\bigsqcup f \in s$ is the function $\lambda i, \bigsqcup_{f \in s} f(i)$.

Pi.infSet instance

{α : Type*} {β : α → Type*} [∀ i, InfSet (β i)] : InfSet (∀ i, β i)

Full source

instance Pi.infSet {α : Type*} {β : α → Type*} [∀ i, InfSet (β i)] : InfSet (∀ i, β i) :=
  ⟨fun s i => ⨅ f : s, (f : ∀ i, β i) i⟩

Pointwise Infimum Structure on Product Types

Informal description

For any family of types $\beta : \alpha \to \text{Type}$ where each $\beta_i$ has an infimum structure, the product type $\prod_{i} \beta_i$ inherits an infimum structure defined pointwise. That is, for any set $s$ of functions in $\prod_{i} \beta_i$, the infimum $\bigsqcap f \in s$ is the function $\lambda i, \bigsqcap_{f \in s} f(i)$.

Pi.instCompleteLattice instance

{α : Type*} {β : α → Type*} [∀ i, CompleteLattice (β i)] : CompleteLattice (∀ i, β i)

Full source

instance Pi.instCompleteLattice {α : Type*} {β : α → Type*} [∀ i, CompleteLattice (β i)] :
    CompleteLattice (∀ i, β i) where
  __ := instBoundedOrder
  le_sSup s f hf := fun i => le_iSup (fun f : s => (f : ∀ i, β i) i) ⟨f, hf⟩
  sInf_le s f hf := fun i => iInf_le (fun f : s => (f : ∀ i, β i) i) ⟨f, hf⟩
  sSup_le _ _ hf := fun i => iSup_le fun g => hf g g.2 i
  le_sInf _ _ hf := fun i => le_iInf fun g => hf g g.2 i

Complete Lattice Structure on Product Types

Informal description

For any family of types $\beta : \alpha \to \text{Type}$ where each $\beta_i$ is a complete lattice, the product type $\prod_{i} \beta_i$ is also a complete lattice with pointwise supremum and infimum operations. That is, for any subset $s$ of functions in $\prod_{i} \beta_i$, the supremum $\bigsqcup s$ is the function $\lambda i, \bigsqcup_{f \in s} f(i)$ and the infimum $\bigsqcap s$ is the function $\lambda i, \bigsqcap_{f \in s} f(i)$.

sSup_apply theorem

 {α : Type*} {β : α → Type*} [∀ i, SupSet (β i)] {s : Set (∀ a, β a)} {a : α} : (sSup s) a = ⨆ f : s, (f : ∀ a, β a) a

Full source

@[simp]
theorem sSup_apply {α : Type*} {β : α → Type*} [∀ i, SupSet (β i)] {s : Set (∀ a, β a)} {a : α} :
    (sSup s) a = ⨆ f : s, (f : ∀ a, β a) a :=
  rfl

Pointwise Evaluation of Supremum of Functions

Informal description

Let $\alpha$ be a type and $\beta : \alpha \to \text{Type}$ be a family of types where each $\beta_i$ has a supremum operator. For any set $s$ of functions in $\prod_{i} \beta_i$ and any $a \in \alpha$, the evaluation of the supremum of $s$ at $a$ equals the supremum of the evaluations of all functions in $s$ at $a$. That is, $$(\bigsqcup s)(a) = \bigsqcup_{f \in s} f(a).$$

sInf_apply theorem

 {α : Type*} {β : α → Type*} [∀ i, InfSet (β i)] {s : Set (∀ a, β a)} {a : α} : sInf s a = ⨅ f : s, (f : ∀ a, β a) a

Full source

@[simp]
theorem sInf_apply {α : Type*} {β : α → Type*} [∀ i, InfSet (β i)] {s : Set (∀ a, β a)} {a : α} :
    sInf s a = ⨅ f : s, (f : ∀ a, β a) a :=
  rfl

Pointwise Infimum Evaluation for Function Sets

Informal description

Let $\alpha$ be a type and $\beta : \alpha \to \text{Type}$ be a family of types where each $\beta_i$ has an infimum structure. For any set $s$ of functions in $\prod_{a \in \alpha} \beta_a$ and any $a \in \alpha$, the infimum of $s$ evaluated at $a$ equals the infimum of the evaluations of all functions in $s$ at $a$. That is, \[ (\bigsqcap s)(a) = \bigsqcap_{f \in s} f(a). \]

iSup_apply theorem

 {α : Type*} {β : α → Type*} {ι : Sort*} [∀ i, SupSet (β i)] {f : ι → ∀ a, β a} {a : α} : (⨆ i, f i) a = ⨆ i, f i a

Full source

@[simp]
theorem iSup_apply {α : Type*} {β : α → Type*} {ι : Sort*} [∀ i, SupSet (β i)] {f : ι → ∀ a, β a}
    {a : α} : (⨆ i, f i) a = ⨆ i, f i a := by
  rw [iSup, sSup_apply, iSup, iSup, ← image_eq_range (fun f : ∀ i, β i => f a) (range f), ←
    range_comp]; rfl

Pointwise Evaluation of Indexed Supremum of Functions: $(\bigsqcup_i f_i)(a) = \bigsqcup_i f_i(a)$

Informal description

Let $\alpha$ be a type and $\beta : \alpha \to \text{Type}$ be a family of types where each $\beta_i$ has a supremum operator. For any indexed family of functions $f : \iota \to \prod_{a \in \alpha} \beta_a$ and any $a \in \alpha$, the evaluation of the supremum of $f$ at $a$ equals the supremum of the evaluations of all functions in $f$ at $a$. That is, $$ \left(\bigsqcup_{i} f_i\right)(a) = \bigsqcup_{i} f_i(a). $$

iInf_apply theorem

 {α : Type*} {β : α → Type*} {ι : Sort*} [∀ i, InfSet (β i)] {f : ι → ∀ a, β a} {a : α} : (⨅ i, f i) a = ⨅ i, f i a

Full source

@[simp]
theorem iInf_apply {α : Type*} {β : α → Type*} {ι : Sort*} [∀ i, InfSet (β i)] {f : ι → ∀ a, β a}
    {a : α} : (⨅ i, f i) a = ⨅ i, f i a :=
  @iSup_apply α (fun i => (β i)ᵒᵈ) _ _ _ _

Pointwise Evaluation of Indexed Infimum of Functions: $(\bigsqcap_i f_i)(a) = \bigsqcap_i f_i(a)$

Informal description

Let $\alpha$ be a type and $\beta : \alpha \to \text{Type}$ be a family of types where each $\beta_i$ has an infimum structure. For any indexed family of functions $f : \iota \to \prod_{a \in \alpha} \beta_a$ and any $a \in \alpha$, the evaluation of the infimum of $f$ at $a$ equals the infimum of the evaluations of all functions in $f$ at $a$. That is, \[ \left(\bigsqcap_{i} f_i\right)(a) = \bigsqcap_{i} f_i(a). \]

unary_relation_sSup_iff theorem

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

Full source

theorem unary_relation_sSup_iff {α : Type*} (s : Set (α → Prop)) {a : α} :
    sSupsSup s a ↔ ∃ r : α → Prop, r ∈ s ∧ r a := by
  rw [sSup_apply]
  simp [← eq_iff_iff]

Supremum of Unary Predicates Evaluates to Existential Quantification

Informal description

For any set $s$ of unary predicates (i.e., functions from a type $\alpha$ to propositions) and any element $a \in \alpha$, the supremum of $s$ evaluated at $a$ holds if and only if there exists a predicate $r \in s$ such that $r(a)$ holds. In other words, $$\left(\bigsqcup s\right)(a) \leftrightarrow \exists r \in s, r(a).$$

unary_relation_sInf_iff theorem

{α : Type*} (s : Set (α → Prop)) {a : α} : sInf s a ↔ ∀ r : α → Prop, r ∈ s → r a

Full source

theorem unary_relation_sInf_iff {α : Type*} (s : Set (α → Prop)) {a : α} :
    sInfsInf s a ↔ ∀ r : α → Prop, r ∈ s → r a := by
  rw [sInf_apply]
  simp [← eq_iff_iff]

Characterization of Infimum for Unary Predicates

Informal description

For any type $\alpha$ and a set $s$ of unary predicates on $\alpha$, the infimum of $s$ evaluated at an element $a \in \alpha$ holds if and only if every predicate $r \in s$ satisfies $r(a)$. In other words, \[ \left(\bigsqcap s\right)(a) \leftrightarrow \forall r \in s, r(a). \]

binary_relation_sSup_iff theorem

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

Full source

theorem binary_relation_sSup_iff {α β : Type*} (s : Set (α → β → Prop)) {a : α} {b : β} :
    sSupsSup s a b ↔ ∃ r : α → β → Prop, r ∈ s ∧ r a b := by
  rw [sSup_apply]
  simp [← eq_iff_iff]

Supremum of Binary Relations Evaluates to Existential Quantification

Informal description

For any set $s$ of binary relations from $\alpha$ to $\beta$ (i.e., functions $\alpha \to \beta \to \mathrm{Prop}$), and for any elements $a \in \alpha$ and $b \in \beta$, the supremum of $s$ evaluated at $(a, b)$ holds if and only if there exists a relation $r \in s$ such that $r(a, b)$ holds. In other words: $$ \left(\bigsqcup s\right)(a, b) \leftrightarrow \exists r \in s, r(a, b). $$

binary_relation_sInf_iff theorem

 {α β : Type*} (s : Set (α → β → Prop)) {a : α} {b : β} : sInf s a b ↔ ∀ r : α → β → Prop, r ∈ s → r a b

Full source

theorem binary_relation_sInf_iff {α β : Type*} (s : Set (α → β → Prop)) {a : α} {b : β} :
    sInfsInf s a b ↔ ∀ r : α → β → Prop, r ∈ s → r a b := by
  rw [sInf_apply]
  simp [← eq_iff_iff]

Characterization of Infimum for Binary Relations: $(\bigsqcap s)(a, b) \leftrightarrow \forall r \in s, r(a, b)$

Informal description

For any type $\alpha$ and $\beta$, and for any set $s$ of binary relations from $\alpha$ to $\beta$ (i.e., functions $\alpha \to \beta \to \mathrm{Prop}$), the infimum of $s$ evaluated at $(a, b) \in \alpha \times \beta$ holds if and only if for every relation $r \in s$, the relation $r(a, b)$ holds. In other words: \[ \left(\bigsqcap s\right)(a, b) \leftrightarrow \forall r \in s, r(a, b). \]

Monotone.sSup theorem

(hs : ∀ f ∈ s, Monotone f) : Monotone (sSup s)

Full source

protected lemma Monotone.sSup (hs : ∀ f ∈ s, Monotone f) : Monotone (sSup s) :=
  fun _ _ h ↦ iSup_mono fun f ↦ hs f f.2 h

Monotonicity of the Supremum of Monotone Functions

Informal description

For any set $s$ of functions from a preorder $\alpha$ to a complete lattice $\beta$, if every function $f \in s$ is monotone, then the supremum of $s$ (i.e., the pointwise supremum $\bigsqcup_{f \in s} f$) is also a monotone function.

Monotone.sInf theorem

(hs : ∀ f ∈ s, Monotone f) : Monotone (sInf s)

Full source

protected lemma Monotone.sInf (hs : ∀ f ∈ s, Monotone f) : Monotone (sInf s) :=
  fun _ _ h ↦ iInf_mono fun f ↦ hs f f.2 h

Monotonicity of Infimum of Monotone Functions

Informal description

Let $s$ be a set of functions from a preorder $\alpha$ to a complete lattice $\beta$. If every function $f \in s$ is monotone, then the infimum of $s$ (taken pointwise) is also a monotone function. That is, for any $a, b \in \alpha$ with $a \leq b$, we have $\bigsqcap_{f \in s} f(a) \leq \bigsqcap_{f \in s} f(b)$.

Antitone.sSup theorem

(hs : ∀ f ∈ s, Antitone f) : Antitone (sSup s)

Full source

protected lemma Antitone.sSup (hs : ∀ f ∈ s, Antitone f) : Antitone (sSup s) :=
  fun _ _ h ↦ iSup_mono fun f ↦ hs f f.2 h

Antitonicity of Pointwise Supremum of Antitone Functions

Informal description

For any set $s$ of functions from a preorder $\alpha$ to a complete lattice $\beta$, if every function $f \in s$ is antitone, then the supremum of $s$ (taken pointwise) is also an antitone function. That is, for any $a, b \in \alpha$ with $a \leq b$, we have $\bigsqcup_{f \in s} f(b) \leq \bigsqcup_{f \in s} f(a)$.

Antitone.sInf theorem

(hs : ∀ f ∈ s, Antitone f) : Antitone (sInf s)

Full source

protected lemma Antitone.sInf (hs : ∀ f ∈ s, Antitone f) : Antitone (sInf s) :=
  fun _ _ h ↦ iInf_mono fun f ↦ hs f f.2 h

Pointwise Infimum Preserves Antitonicity

Informal description

Let $s$ be a set of functions from a preorder $\alpha$ to a complete lattice $\beta$. If every function $f \in s$ is antitone (i.e., $a \leq b$ implies $f(b) \leq f(a)$ for all $a, b \in \alpha$), then the infimum of $s$ (taken pointwise) is also an antitone function. That is, for any $a, b \in \alpha$ with $a \leq b$, we have $\bigsqcap_{f \in s} f(b) \leq \bigsqcap_{f \in s} f(a)$.

Monotone.iSup theorem

(hf : ∀ i, Monotone (f i)) : Monotone (⨆ i, f i)

Full source

protected lemma Monotone.iSup (hf : ∀ i, Monotone (f i)) : Monotone (⨆ i, f i) :=
  Monotone.sSup (by simpa)

Monotonicity of Pointwise Supremum of Monotone Functions

Informal description

For any indexed family of functions $f_i : \alpha \to \beta$ from a preorder $\alpha$ to a complete lattice $\beta$, if each $f_i$ is monotone, then the pointwise supremum $\bigsqcup_i f_i$ is also a monotone function. That is, for any $a, b \in \alpha$ with $a \leq b$, we have $\bigsqcup_i f_i(a) \leq \bigsqcup_i f_i(b)$.

Monotone.iInf theorem

(hf : ∀ i, Monotone (f i)) : Monotone (⨅ i, f i)

Full source

protected lemma Monotone.iInf (hf : ∀ i, Monotone (f i)) : Monotone (⨅ i, f i) :=
  Monotone.sInf (by simpa)

Monotonicity of Infimum of Monotone Functions

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of monotone functions from a preorder $\alpha$ to a complete lattice $\beta$. Then the infimum function $\bigsqcap_{i} f_i$ (defined pointwise) is also monotone. That is, for any $a, b \in \alpha$ with $a \leq b$, we have $\left(\bigsqcap_{i} f_i\right)(a) \leq \left(\bigsqcap_{i} f_i\right)(b)$.

Antitone.iSup theorem

(hf : ∀ i, Antitone (f i)) : Antitone (⨆ i, f i)

Full source

protected lemma Antitone.iSup (hf : ∀ i, Antitone (f i)) : Antitone (⨆ i, f i) :=
  Antitone.sSup (by simpa)

Pointwise Supremum Preserves Antitonicity for Indexed Family

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of antitone functions from a preorder $\alpha$ to a complete lattice $\beta$. Then the pointwise supremum function $\bigsqcup_i f_i$ is also antitone. That is, for any $a, b \in \alpha$ with $a \leq b$, we have $(\bigsqcup_i f_i)(b) \leq (\bigsqcup_i f_i)(a)$.

Antitone.iInf theorem

(hf : ∀ i, Antitone (f i)) : Antitone (⨅ i, f i)

Full source

protected lemma Antitone.iInf (hf : ∀ i, Antitone (f i)) : Antitone (⨅ i, f i) :=
  Antitone.sInf (by simpa)

Pointwise Infimum Preserves Antitonicity for Indexed Family

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of antitone functions from a preorder $\alpha$ to a complete lattice $\beta$. Then the pointwise infimum function $\bigsqcap_i f_i$ is also antitone. That is, for any $a, b \in \alpha$ with $a \leq b$, we have $(\bigsqcap_i f_i)(b) \leq (\bigsqcap_i f_i)(a)$.

Prod.supSet instance

[SupSet α] [SupSet β] : SupSet (α × β)

Full source

instance supSet [SupSet α] [SupSet β] : SupSet (α × β) :=
  ⟨fun s => (sSup (Prod.fst '' s), sSup (Prod.snd '' s))⟩

Supremum Operator on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with supremum operators, the product type $\alpha \times \beta$ is also equipped with a supremum operator. The supremum of a set $s \subseteq \alpha \times \beta$ is given by the pair $(sSup (\pi_1 \ '' s), sSup (\pi_2 \ '' s))$, where $\pi_1$ and $\pi_2$ are the first and second projections respectively, and $\ ''$ denotes the image of a set under a function.

Prod.infSet instance

[InfSet α] [InfSet β] : InfSet (α × β)

Full source

instance infSet [InfSet α] [InfSet β] : InfSet (α × β) :=
  ⟨fun s => (sInf (Prod.fst '' s), sInf (Prod.snd '' s))⟩

Infimum Structure on Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum structures, the product type $\alpha \times \beta$ is also equipped with an infimum structure. The infimum of a set $s \subseteq \alpha \times \beta$ is given by the pair $(sInf (\pi_1 \ '' s), sInf (\pi_2 \ '' s))$, where $\pi_1$ and $\pi_2$ are the first and second projections respectively, and $\ ''$ denotes the image of a set under a function.

Prod.fst_sInf theorem

[InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).fst = sInf (Prod.fst '' s)

Full source

theorem fst_sInf [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).fst = sInf (Prod.fstProd.fst '' s) :=
  rfl

First Projection of Infimum Equals Infimum of First Projections

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum structures, and for any set $s \subseteq \alpha \times \beta$, the first projection of the infimum of $s$ equals the infimum of the image of $s$ under the first projection. In symbols: $$(\inf s).1 = \inf \{a \mid (a, b) \in s\}$$

Prod.snd_sInf theorem

[InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).snd = sInf (Prod.snd '' s)

Full source

theorem snd_sInf [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).snd = sInf (Prod.sndProd.snd '' s) :=
  rfl

Second Projection Preserves Infimum in Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum structures, and for any set $s \subseteq \alpha \times \beta$, the second component of the infimum of $s$ equals the infimum of the image of $s$ under the second projection. That is, $(\inf s).2 = \inf \{y \mid \exists x, (x,y) \in s\}$.

Prod.swap_sInf theorem

[InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).swap = sInf (Prod.swap '' s)

Full source

theorem swap_sInf [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).swap = sInf (Prod.swapProd.swap '' s) :=
  Prod.ext (congr_arg sInf <| image_comp Prod.fst swap s)
    (congr_arg sInf <| image_comp Prod.snd swap s)

Swap Commutes with Infimum in Product Types

Informal description

For any types $\alpha$ and $\beta$ equipped with infimum structures, and for any set $s \subseteq \alpha \times \beta$, the swap of the infimum of $s$ equals the infimum of the image of $s$ under the swap operation. That is, $$(\inf s).\text{swap} = \inf \{(b, a) \mid (a, b) \in s\}.$$

Prod.fst_sSup theorem

[SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).fst = sSup (Prod.fst '' s)

Full source

theorem fst_sSup [SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).fst = sSup (Prod.fstProd.fst '' s) :=
  rfl

First Projection of Supremum Equals Supremum of First Projections

Informal description

For any types $\alpha$ and $\beta$ equipped with supremum operators, and for any set $s \subseteq \alpha \times \beta$, the first projection of the supremum of $s$ equals the supremum of the image of $s$ under the first projection. That is, $(\bigsqcup s).1 = \bigsqcup \{x.1 \mid x \in s\}$.

Prod.snd_sSup theorem

[SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).snd = sSup (Prod.snd '' s)

Full source

theorem snd_sSup [SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).snd = sSup (Prod.sndProd.snd '' s) :=
  rfl

Second Component of Supremum in Product Space Equals Supremum of Second Projection

Informal description

Let $\alpha$ and $\beta$ be types equipped with supremum operators. For any set $s \subseteq \alpha \times \beta$, the second component of its supremum equals the supremum of the image of $s$ under the second projection, i.e., $$(\mathrm{sSup}\, s).2 = \mathrm{sSup}\, (\pi_2 \ '' s)$$ where $\pi_2$ denotes the second projection map from $\alpha \times \beta$ to $\beta$.

Prod.swap_sSup theorem

[SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).swap = sSup (Prod.swap '' s)

Full source

theorem swap_sSup [SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).swap = sSup (Prod.swapProd.swap '' s) :=
  Prod.ext (congr_arg sSup <| image_comp Prod.fst swap s)
    (congr_arg sSup <| image_comp Prod.snd swap s)

Swap Commutes with Supremum in Product Space

Informal description

For any types $\alpha$ and $\beta$ equipped with supremum operators, and for any set $s \subseteq \alpha \times \beta$, the swap of the supremum of $s$ equals the supremum of the image of $s$ under the swap operation. That is, $(\mathrm{sSup}\, s)^\mathrm{swap} = \mathrm{sSup}\, \{x^\mathrm{swap} \mid x \in s\}$.

Prod.fst_iInf theorem

[InfSet α] [InfSet β] (f : ι → α × β) : (iInf f).fst = ⨅ i, (f i).fst

Full source

theorem fst_iInf [InfSet α] [InfSet β] (f : ι → α × β) : (iInf f).fst = ⨅ i, (f i).fst :=
  congr_arg sInf (range_comp _ _).symm

First Projection of Infimum Equals Infimum of First Projections

Informal description

For any indexed family of pairs $f : \iota \to \alpha \times \beta$ where $\alpha$ and $\beta$ are types equipped with infimum structures, the first projection of the infimum of $f$ equals the infimum of the first projections of the pairs. That is, $(\bigsqcap_i f_i).\mathrm{fst} = \bigsqcap_i (f_i.\mathrm{fst})$.

Prod.snd_iInf theorem

[InfSet α] [InfSet β] (f : ι → α × β) : (iInf f).snd = ⨅ i, (f i).snd

Full source

theorem snd_iInf [InfSet α] [InfSet β] (f : ι → α × β) : (iInf f).snd = ⨅ i, (f i).snd :=
  congr_arg sInf (range_comp _ _).symm

Second Component of Infimum Equals Infimum of Second Components

Informal description

For any indexed family of pairs $f : \iota \to \alpha \times \beta$ where $\alpha$ and $\beta$ are types equipped with infimum structures, the second component of the infimum of $f$ equals the infimum of the second components of the pairs in $f$. That is, $$(\bigsqcap_i f_i).2 = \bigsqcap_i (f_i.2).$$

Prod.swap_iInf theorem

[InfSet α] [InfSet β] (f : ι → α × β) : (iInf f).swap = ⨅ i, (f i).swap

Full source

theorem swap_iInf [InfSet α] [InfSet β] (f : ι → α × β) : (iInf f).swap = ⨅ i, (f i).swap := by
  simp_rw [iInf, swap_sInf, ← range_comp, comp_def]

Swapping Commutes with Indexed Infimum in Product Types

Informal description

For any indexed family of pairs $f : \iota \to \alpha \times \beta$ where $\alpha$ and $\beta$ are types equipped with infimum structures, swapping the components of the infimum of $f$ is equal to the infimum of the family obtained by swapping the components of each pair in $f$. That is, $$(\bigsqcap_i f_i).\mathrm{swap} = \bigsqcap_i (f_i.\mathrm{swap}).$$

Prod.iInf_mk theorem

[InfSet α] [InfSet β] (f : ι → α) (g : ι → β) : ⨅ i, (f i, g i) = (⨅ i, f i, ⨅ i, g i)

Full source

theorem iInf_mk [InfSet α] [InfSet β] (f : ι → α) (g : ι → β) :
    ⨅ i, (f i, g i) = (⨅ i, f i, ⨅ i, g i) :=
  congr_arg₂ Prod.mk (fst_iInf _) (snd_iInf _)

Infimum of Pairwise Elements Equals Pair of Infima

Informal description

For any indexed families of elements $f : \iota \to \alpha$ and $g : \iota \to \beta$ where $\alpha$ and $\beta$ are types equipped with infimum structures, the infimum of the pairs $(f_i, g_i)$ is equal to the pair of the infima of $f$ and $g$ respectively. That is, $$\bigsqcap_i (f_i, g_i) = \left(\bigsqcap_i f_i, \bigsqcap_i g_i\right).$$

Prod.fst_iSup theorem

[SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).fst = ⨆ i, (f i).fst

Full source

theorem fst_iSup [SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).fst = ⨆ i, (f i).fst :=
  congr_arg sSup (range_comp _ _).symm

First Projection Commutes with Indexed Supremum

Informal description

For any indexed family of pairs $f : \iota \to \alpha \times \beta$ where $\alpha$ and $\beta$ are types equipped with supremum operators, the first projection of the supremum of $f$ equals the supremum of the first projections of the pairs, i.e., $$(\bigsqcup_i f_i).1 = \bigsqcup_i (f_i.1).$$

Prod.snd_iSup theorem

[SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).snd = ⨆ i, (f i).snd

Full source

theorem snd_iSup [SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).snd = ⨆ i, (f i).snd :=
  congr_arg sSup (range_comp _ _).symm

Second Component of Supremum of Pairs Equals Supremum of Second Components

Informal description

For any indexed family of pairs $f : \iota \to \alpha \times \beta$ where $\alpha$ and $\beta$ are types equipped with supremum operators, the second component of the supremum of $f$ is equal to the supremum of the second components of the pairs in the family. That is, $(\bigsqcup_i f_i).2 = \bigsqcup_i (f_i.2)$.

Prod.swap_iSup theorem

[SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).swap = ⨆ i, (f i).swap

Full source

theorem swap_iSup [SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).swap = ⨆ i, (f i).swap := by
  simp_rw [iSup, swap_sSup, ← range_comp, comp_def]

Swap Commutes with Indexed Supremum in Product Space

Informal description

For any indexed family of pairs $f : \iota \to \alpha \times \beta$ where $\alpha$ and $\beta$ are types equipped with supremum operators, the swap of the supremum of $f$ equals the supremum of the swaps of the pairs in the family. That is, $$(\bigsqcup_i f_i)^\mathrm{swap} = \bigsqcup_i (f_i^\mathrm{swap}).$$

Prod.iSup_mk theorem

[SupSet α] [SupSet β] (f : ι → α) (g : ι → β) : ⨆ i, (f i, g i) = (⨆ i, f i, ⨆ i, g i)

Full source

theorem iSup_mk [SupSet α] [SupSet β] (f : ι → α) (g : ι → β) :
    ⨆ i, (f i, g i) = (⨆ i, f i, ⨆ i, g i) :=
  congr_arg₂ Prod.mk (fst_iSup _) (snd_iSup _)

Supremum of Pairwise Products Equals Pair of Suprema

Informal description

For any indexed families of elements $f : \iota \to \alpha$ and $g : \iota \to \beta$ where $\alpha$ and $\beta$ are types equipped with supremum operators, the supremum of the pairs $(f_i, g_i)$ is equal to the pair of the suprema of $f$ and $g$ individually. That is, $$\bigsqcup_i (f_i, g_i) = \left(\bigsqcup_i f_i, \bigsqcup_i g_i\right).$$

Prod.instCompleteLattice instance

[CompleteLattice α] [CompleteLattice β] : CompleteLattice (α × β)

Full source

instance instCompleteLattice [CompleteLattice α] [CompleteLattice β] : CompleteLattice (α × β) where
  __ := instBoundedOrder α β
  le_sSup _ _ hab := ⟨le_sSup <| mem_image_of_mem _ hab, le_sSup <| mem_image_of_mem _ hab⟩
  sSup_le _ _ h :=
    ⟨sSup_le <| forall_mem_image.2 fun p hp => (h p hp).1,
      sSup_le <| forall_mem_image.2 fun p hp => (h p hp).2⟩
  sInf_le _ _ hab := ⟨sInf_le <| mem_image_of_mem _ hab, sInf_le <| mem_image_of_mem _ hab⟩
  le_sInf _ _ h :=
    ⟨le_sInf <| forall_mem_image.2 fun p hp => (h p hp).1,
      le_sInf <| forall_mem_image.2 fun p hp => (h p hp).2⟩

Complete Lattice Structure on Product Types

Informal description

For any complete lattices $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is also a complete lattice, where the supremum and infimum operations are defined componentwise. That is, for any subset $S \subseteq \alpha \times \beta$, its supremum is $(\bigvee_{(a,b) \in S} a, \bigvee_{(a,b) \in S} b)$ and its infimum is $(\bigwedge_{(a,b) \in S} a, \bigwedge_{(a,b) \in S} b)$.

sInf_prod theorem

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

Full source

lemma sInf_prod [InfSet α] [InfSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) :
    sInf (s ×ˢ t) = (sInf s, sInf t) :=
congr_arg₂ Prod.mk (congr_arg sInf <| fst_image_prod _ ht) (congr_arg sInf <| snd_image_prod hs _)

Infimum of Cartesian Product Equals Pair of Infima

Informal description

Let $\alpha$ and $\beta$ be types equipped with infimum structures. For any nonempty set $s \subseteq \alpha$ and nonempty set $t \subseteq \beta$, the infimum of their Cartesian product $s \times t$ is equal to the pair of infima $(\inf s, \inf t)$. In symbols: $$\inf (s \times t) = (\inf s, \inf t)$$

sSup_prod theorem

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

Full source

lemma sSup_prod [SupSet α] [SupSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) :
    sSup (s ×ˢ t) = (sSup s, sSup t) :=
congr_arg₂ Prod.mk (congr_arg sSup <| fst_image_prod _ ht) (congr_arg sSup <| snd_image_prod hs _)

Supremum of Cartesian Product is Componentwise Supremum

Informal description

For any nonempty sets $s \subseteq \alpha$ and $t \subseteq \beta$ in types equipped with supremum operators, the supremum of their Cartesian product $s \times t$ is the pair consisting of the suprema of $s$ and $t$ respectively, i.e., \[ \mathrm{sSup}(s \times t) = (\mathrm{sSup}\, s, \mathrm{sSup}\, t). \]

Function.Injective.completeLattice abbrev

 [Max α] [Min α] [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, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) : CompleteLattice α

Full source

/-- Pullback a `CompleteLattice` along an injection. -/
protected abbrev Function.Injective.completeLattice [Max α] [Min α] [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, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a)
    (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : CompleteLattice α where
  -- we cannot use BoundedOrder.lift here as the `LE` instance doesn't exist yet
  __ := hf.lattice f map_sup map_inf
  le_sSup _ a h := (le_iSup₂ a h).trans (map_sSup _).ge
  sSup_le _ _ h := (map_sSup _).trans_le <| iSup₂_le h
  sInf_le _ a h := (map_sInf _).trans_le <| iInf₂_le a h
  le_sInf _ _ h := (le_iInf₂ h).trans (map_sInf _).ge
  top := ⊤
  le_top _ := (@le_top β _ _ _).trans map_top.ge
  bot := ⊥
  bot_le _ := map_bot.le.trans bot_le

Injective Complete Lattice-Preserving Function Induces Complete Lattice Structure

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is a complete lattice. Given an injective function $f : \alpha \to \beta$ that preserves: 1. Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, 2. Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, 3. Arbitrary suprema: $f(\mathrm{sSup}\, s) = \bigsqcup_{a \in s} f(a)$ for any set $s \subseteq \alpha$, 4. Arbitrary infima: $f(\mathrm{sInf}\, s) = \bigsqcap_{a \in s} f(a)$ for any set $s \subseteq \alpha$, 5. Top element: $f(\top) = \top$, 6. Bottom element: $f(\bot) = \bot$, then $\alpha$ can be endowed with a complete lattice structure where all operations are defined via $f$.

Mathlib.Order.CompleteLattice.Basic

Naming conventions

Notation