Mathlib.Order.ConditionallyCompleteLattice.Indexed

WithTop.iInf_empty theorem

[IsEmpty ι] [InfSet α] (f : ι → WithTop α) : ⨅ i, f i = ⊤

Full source

@[simp]
theorem WithTop.iInf_empty [IsEmpty ι] [InfSet α] (f : ι → WithTop α) :
    ⨅ i, f i = ⊤ := by rw [iInf, range_eq_empty, WithTop.sInf_empty]

Infimum over Empty Index Set in `WithTop α` is Top Element

Informal description

For any type `ι` that is empty (i.e., `IsEmpty ι`) and any type `α` with an infimum operation (i.e., `InfSet α`), the infimum of any function `f : ι → WithTop α` over the empty index set `ι` is equal to the top element `⊤` of `WithTop α`.

WithTop.coe_iInf theorem

[Nonempty ι] [InfSet α] {f : ι → α} (hf : BddBelow (range f)) : ↑(⨅ i, f i) = (⨅ i, f i : WithTop α)

Full source

@[norm_cast]
theorem WithTop.coe_iInf [Nonempty ι] [InfSet α] {f : ι → α} (hf : BddBelow (range f)) :
    ↑(⨅ i, f i) = (⨅ i, f i : WithTop α) := by
  rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]

Embedding of Infimum in WithTop Preserves Infimum for Bounded Below Functions

Informal description

Let $ι$ be a nonempty type, $α$ a type with an infimum operation, and $f : ι → α$ a function with bounded below range. Then the canonical embedding of the infimum of $f$ in $α$ equals the infimum of $f$ in $\mathrm{WithTop}\,α$. That is, $\uparrow(\bigsqcap_{i} f(i)) = \bigsqcap_{i} (f(i) : \mathrm{WithTop}\,α)$.

WithTop.coe_iSup theorem

[SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) : ↑(⨆ i, f i) = (⨆ i, f i : WithTop α)

Full source

@[norm_cast]
theorem WithTop.coe_iSup [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) :
    ↑(⨆ i, f i) = (⨆ i, f i : WithTop α) := by
  rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]

Canonical Embedding Preserves Supremum in WithTop

Informal description

Let $\alpha$ be a type with a supremum operation, and let $f : \iota \to \alpha$ be a function whose range is bounded above. Then the image of the supremum $\bigsqcup_{i} f(i)$ under the canonical embedding $\alpha \to \text{WithTop}\ \alpha$ is equal to the supremum of $f$ computed in $\text{WithTop}\ \alpha$.

WithBot.ciSup_empty theorem

[IsEmpty ι] [SupSet α] (f : ι → WithBot α) : ⨆ i, f i = ⊥

Full source

@[simp]
theorem WithBot.ciSup_empty [IsEmpty ι] [SupSet α] (f : ι → WithBot α) :
    ⨆ i, f i = ⊥ :=
  WithTop.iInf_empty (α := αᵒᵈ) _

Supremum over Empty Index Set in `WithBot α` is Bottom Element

Informal description

For any type `ι` that is empty (i.e., `IsEmpty ι`) and any type `α` with a supremum operation (i.e., `SupSet α`), the supremum of any function `f : ι → WithBot α` over the empty index set `ι` is equal to the bottom element `⊥` of `WithBot α`.

WithBot.coe_iSup theorem

[Nonempty ι] [SupSet α] {f : ι → α} (hf : BddAbove (range f)) : ↑(⨆ i, f i) = (⨆ i, f i : WithBot α)

Full source

@[norm_cast]
theorem WithBot.coe_iSup [Nonempty ι] [SupSet α] {f : ι → α} (hf : BddAbove (range f)) :
    ↑(⨆ i, f i) = (⨆ i, f i : WithBot α) :=
  WithTop.coe_iInf (α := αᵒᵈ) hf

Embedding of Supremum in WithBot Preserves Supremum for Bounded Above Functions

Informal description

Let $\iota$ be a nonempty type, $\alpha$ a type with a supremum operation, and $f : \iota \to \alpha$ a function with bounded above range. Then the canonical embedding of the supremum of $f$ in $\alpha$ equals the supremum of $f$ in $\mathrm{WithBot}\,\alpha$. That is, $\uparrow(\bigsqcup_{i} f(i)) = \bigsqcup_{i} (f(i) : \mathrm{WithBot}\,\alpha)$.

WithBot.coe_iInf theorem

[InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) : ↑(⨅ i, f i) = (⨅ i, f i : WithBot α)

Full source

@[norm_cast]
theorem WithBot.coe_iInf [InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) :
    ↑(⨅ i, f i) = (⨅ i, f i : WithBot α) :=
  WithTop.coe_iSup (α := αᵒᵈ) _ h

Canonical Embedding Preserves Infimum in WithBot

Informal description

Let $\alpha$ be a type with an infimum operation, and let $f : \iota \to \alpha$ be a function whose range is bounded below. Then the image of the infimum $\bigsqcap_{i} f(i)$ under the canonical embedding $\alpha \to \text{WithBot}\ \alpha$ is equal to the infimum of $f$ computed in $\text{WithBot}\ \alpha$.

isLUB_ciSup theorem

[Nonempty ι] {f : ι → α} (H : BddAbove (range f)) : IsLUB (range f) (⨆ i, f i)

Full source

theorem isLUB_ciSup [Nonempty ι] {f : ι → α} (H : BddAbove (range f)) :
    IsLUB (range f) (⨆ i, f i) :=
  isLUB_csSup (range_nonempty f) H

Indexed Supremum is Least Upper Bound in Conditionally Complete Lattice

Informal description

Let $\iota$ be a nonempty type and $f : \iota \to \alpha$ be a function with bounded above range in a conditionally complete lattice $\alpha$. Then the indexed supremum $\bigsqcup_{i} f(i)$ is the least upper bound of the range of $f$.

isLUB_ciSup_set theorem

{f : β → α} {s : Set β} (H : BddAbove (f '' s)) (Hne : s.Nonempty) : IsLUB (f '' s) (⨆ i : s, f i)

Full source

theorem isLUB_ciSup_set {f : β → α} {s : Set β} (H : BddAbove (f '' s)) (Hne : s.Nonempty) :
    IsLUB (f '' s) (⨆ i : s, f i) := by
  rw [← sSup_image']
  exact isLUB_csSup (Hne.image _) H

Supremum of Bounded Nonempty Set is Least Upper Bound

Informal description

Let $f : \beta \to \alpha$ be a function and $s \subseteq \beta$ a nonempty subset. If the image $f(s)$ is bounded above in $\alpha$, then the supremum $\bigsqcup_{i \in s} f(i)$ is the least upper bound of $f(s)$.

isGLB_ciInf theorem

[Nonempty ι] {f : ι → α} (H : BddBelow (range f)) : IsGLB (range f) (⨅ i, f i)

Full source

theorem isGLB_ciInf [Nonempty ι] {f : ι → α} (H : BddBelow (range f)) :
    IsGLB (range f) (⨅ i, f i) :=
  isGLB_csInf (range_nonempty f) H

Greatest Lower Bound Property of Conditionally Complete Infimum

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of elements in a conditionally complete lattice $\alpha$, where $\iota$ is nonempty. If the range of $f$ is bounded below, then the infimum $\bigsqcap_{i} f_i$ is the greatest lower bound of the range of $f$.

isGLB_ciInf_set theorem

{f : β → α} {s : Set β} (H : BddBelow (f '' s)) (Hne : s.Nonempty) : IsGLB (f '' s) (⨅ i : s, f i)

Full source

theorem isGLB_ciInf_set {f : β → α} {s : Set β} (H : BddBelow (f '' s)) (Hne : s.Nonempty) :
    IsGLB (f '' s) (⨅ i : s, f i) :=
  isLUB_ciSup_set (α := αᵒᵈ) H Hne

Greatest Lower Bound Property of Conditionally Complete Infimum over a Set

Informal description

Let $f : \beta \to \alpha$ be a function and $s \subseteq \beta$ a nonempty subset. If the image $f(s)$ is bounded below in $\alpha$, then the infimum $\bigsqcap_{i \in s} f(i)$ is the greatest lower bound of $f(s)$.

ciSup_le_iff theorem

[Nonempty ι] {f : ι → α} {a : α} (hf : BddAbove (range f)) : iSup f ≤ a ↔ ∀ i, f i ≤ a

Full source

theorem ciSup_le_iff [Nonempty ι] {f : ι → α} {a : α} (hf : BddAbove (range f)) :
    iSupiSup f ≤ a ↔ ∀ i, f i ≤ a :=
  (isLUB_le_iff <| isLUB_ciSup hf).trans forall_mem_range

Characterization of Supremum Bound in Conditionally Complete Lattices: $\bigsqcup_i f(i) \leq a \leftrightarrow \forall i, f(i) \leq a$

Informal description

Let $\iota$ be a nonempty type, $f : \iota \to \alpha$ a function with bounded above range in a conditionally complete lattice $\alpha$, and $a \in \alpha$. Then the indexed supremum satisfies $\bigsqcup_{i} f(i) \leq a$ if and only if $f(i) \leq a$ for all $i \in \iota$.

le_ciInf_iff theorem

[Nonempty ι] {f : ι → α} {a : α} (hf : BddBelow (range f)) : a ≤ iInf f ↔ ∀ i, a ≤ f i

Full source

theorem le_ciInf_iff [Nonempty ι] {f : ι → α} {a : α} (hf : BddBelow (range f)) :
    a ≤ iInf f ↔ ∀ i, a ≤ f i :=
  (le_isGLB_iff <| isGLB_ciInf hf).trans forall_mem_range

Characterization of Lower Bounds via Conditionally Complete Infimum

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of elements in a conditionally complete lattice $\alpha$, where $\iota$ is nonempty. If the range of $f$ is bounded below, then an element $a \in \alpha$ satisfies $a \leq \bigsqcap_{i} f_i$ if and only if $a \leq f_i$ for all $i \in \iota$.

ciSup_set_le_iff theorem

 {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty) (hf : BddAbove (f '' s)) :
  ⨆ i : s, f i ≤ a ↔ ∀ i ∈ s, f i ≤ a

Full source

theorem ciSup_set_le_iff {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty)
    (hf : BddAbove (f '' s)) : ⨆ i : s, f i⨆ i : s, f i ≤ a ↔ ∀ i ∈ s, f i ≤ a :=
  (isLUB_le_iff <| isLUB_ciSup_set hf hs).trans forall_mem_image

Characterization of Supremum Bound for Nonempty Bounded Sets: $\bigsqcup_{i \in s} f(i) \leq a \leftrightarrow \forall i \in s, f(i) \leq a$

Informal description

Let $\alpha$ be a conditionally complete lattice, $\iota$ a type, $s \subseteq \iota$ a nonempty subset, and $f : \iota \to \alpha$ a function such that $f(s)$ is bounded above. Then the supremum $\bigsqcup_{i \in s} f(i) \leq a$ if and only if $f(i) \leq a$ for all $i \in s$.

le_ciInf_set_iff theorem

 {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty) (hf : BddBelow (f '' s)) :
  (a ≤ ⨅ i : s, f i) ↔ ∀ i ∈ s, a ≤ f i

Full source

theorem le_ciInf_set_iff {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty)
    (hf : BddBelow (f '' s)) : (a ≤ ⨅ i : s, f i) ↔ ∀ i ∈ s, a ≤ f i :=
  (le_isGLB_iff <| isGLB_ciInf_set hf hs).trans forall_mem_image

Characterization of Lower Bounds via Conditionally Complete Infimum over Nonempty Sets: $a \leq \bigsqcap_{i \in s} f(i) \leftrightarrow \forall i \in s, a \leq f(i)$

Informal description

Let $\alpha$ be a conditionally complete lattice, $\iota$ a type, $s \subseteq \iota$ a nonempty subset, and $f : \iota \to \alpha$ a function such that $f(s)$ is bounded below. Then for any $a \in \alpha$, we have $a \leq \bigsqcap_{i \in s} f(i)$ if and only if $a \leq f(i)$ for all $i \in s$.

IsLUB.ciSup_eq theorem

[Nonempty ι] {f : ι → α} (H : IsLUB (range f) a) : ⨆ i, f i = a

Full source

theorem IsLUB.ciSup_eq [Nonempty ι] {f : ι → α} (H : IsLUB (range f) a) : ⨆ i, f i = a :=
  H.csSup_eq (range_nonempty f)

Supremum Equals Least Upper Bound in Conditionally Complete Lattices

Informal description

Let $\iota$ be a nonempty type and $f : \iota \to \alpha$ be a function into a conditionally complete lattice $\alpha$. If $a$ is the least upper bound of the range of $f$, then the supremum of $f$ over $\iota$ equals $a$, i.e., $\bigsqcup_{i} f(i) = a$.

IsLUB.ciSup_set_eq theorem

{s : Set β} {f : β → α} (H : IsLUB (f '' s) a) (Hne : s.Nonempty) : ⨆ i : s, f i = a

Full source

theorem IsLUB.ciSup_set_eq {s : Set β} {f : β → α} (H : IsLUB (f '' s) a) (Hne : s.Nonempty) :
    ⨆ i : s, f i = a :=
  IsLUB.csSup_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f)

Indexed Supremum Equals Least Upper Bound for Nonempty Sets

Informal description

Let $s$ be a nonempty subset of a type $\beta$, and let $f : \beta \to \alpha$ be a function into a conditionally complete lattice $\alpha$. If $a$ is the least upper bound of the image $f(s)$, then the indexed supremum of $f$ over $s$ equals $a$, i.e., $\bigsqcup_{i \in s} f(i) = a$.

IsGLB.ciInf_eq theorem

[Nonempty ι] {f : ι → α} (H : IsGLB (range f) a) : ⨅ i, f i = a

Full source

theorem IsGLB.ciInf_eq [Nonempty ι] {f : ι → α} (H : IsGLB (range f) a) : ⨅ i, f i = a :=
  H.csInf_eq (range_nonempty f)

Greatest Lower Bound Characterizes Infimum in Conditionally Complete Lattices

Informal description

Let $\iota$ be a nonempty type, $f : \iota \to \alpha$ a function into a conditionally complete lattice $\alpha$, and $a \in \alpha$. If $a$ is the greatest lower bound of the range of $f$, then the infimum of $f$ over $\iota$ equals $a$, i.e., $\bigwedge_{i} f(i) = a$.

IsGLB.ciInf_set_eq theorem

{s : Set β} {f : β → α} (H : IsGLB (f '' s) a) (Hne : s.Nonempty) : ⨅ i : s, f i = a

Full source

theorem IsGLB.ciInf_set_eq {s : Set β} {f : β → α} (H : IsGLB (f '' s) a) (Hne : s.Nonempty) :
    ⨅ i : s, f i = a :=
  IsGLB.csInf_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f)

Infimum Equals Greatest Lower Bound for Nonempty Sets

Informal description

Let $s$ be a nonempty subset of $\beta$ and $f \colon \beta \to \alpha$ a function. If $a$ is the greatest lower bound of the image $f(s)$, then the infimum of $f$ over $s$ equals $a$, i.e., $\bigsqcap_{i \in s} f(i) = a$.

ciSup_le theorem

[Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, f x ≤ c) : iSup f ≤ c

Full source

/-- The indexed supremum of a function is bounded above by a uniform bound -/
theorem ciSup_le [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, f x ≤ c) : iSup f ≤ c :=
  csSup_le (range_nonempty f) (by rwa [forall_mem_range])

Indexed supremum is bounded by uniform upper bound

Informal description

Let $\iota$ be a nonempty type and $f : \iota \to \alpha$ be a function into a conditionally complete lattice $\alpha$. If there exists an element $c \in \alpha$ such that $f(x) \leq c$ for all $x \in \iota$, then the indexed supremum satisfies $\bigsqcup_{i \in \iota} f(i) \leq c$.

le_ciSup theorem

{f : ι → α} (H : BddAbove (range f)) (c : ι) : f c ≤ iSup f

Full source

/-- The indexed supremum of a function is bounded below by the value taken at one point -/
theorem le_ciSup {f : ι → α} (H : BddAbove (range f)) (c : ι) : f c ≤ iSup f :=
  le_csSup H (mem_range_self _)

Element is bounded by indexed supremum in conditionally complete lattice

Informal description

Let $f : \iota \to \alpha$ be a function from a type $\iota$ to a conditionally complete lattice $\alpha$. If the range of $f$ is bounded above, then for any $c \in \iota$, the value $f(c)$ is less than or equal to the supremum of $f$, i.e., $f(c) \leq \sup f$.

le_ciSup_of_le theorem

{f : ι → α} (H : BddAbove (range f)) (c : ι) (h : a ≤ f c) : a ≤ iSup f

Full source

theorem le_ciSup_of_le {f : ι → α} (H : BddAbove (range f)) (c : ι) (h : a ≤ f c) : a ≤ iSup f :=
  le_trans h (le_ciSup H c)

Transitivity of element-to-supremum inequality in conditionally complete lattices

Informal description

Let $f : \iota \to \alpha$ be a function from a type $\iota$ to a conditionally complete lattice $\alpha$, and suppose the range of $f$ is bounded above. For any element $a \in \alpha$ and index $c \in \iota$, if $a \leq f(c)$, then $a \leq \sup f$.

ciSup_mono theorem

{f g : ι → α} (B : BddAbove (range g)) (H : ∀ x, f x ≤ g x) : iSup f ≤ iSup g

Full source

/-- The indexed suprema of two functions are comparable if the functions are pointwise comparable -/
theorem ciSup_mono {f g : ι → α} (B : BddAbove (range g)) (H : ∀ x, f x ≤ g x) :
    iSup f ≤ iSup g := by
  cases isEmpty_or_nonempty ι
  · rw [iSup_of_empty', iSup_of_empty']
  · exact ciSup_le fun x => le_ciSup_of_le B x (H x)

Monotonicity of Indexed Supremum in Conditionally Complete Lattices

Informal description

Let $\iota$ be a type and $\alpha$ a conditionally complete lattice. Given two functions $f, g : \iota \to \alpha$ such that the range of $g$ is bounded above and $f(x) \leq g(x)$ for all $x \in \iota$, the indexed supremum satisfies $\bigsqcup_{i \in \iota} f(i) \leq \bigsqcup_{i \in \iota} g(i)$.

le_ciSup_set theorem

{f : β → α} {s : Set β} (H : BddAbove (f '' s)) {c : β} (hc : c ∈ s) : f c ≤ ⨆ i : s, f i

Full source

theorem le_ciSup_set {f : β → α} {s : Set β} (H : BddAbove (f '' s)) {c : β} (hc : c ∈ s) :
    f c ≤ ⨆ i : s, f i :=
  (le_csSup H <| mem_image_of_mem f hc).trans_eq sSup_image'

Element-wise upper bound for supremum over a set

Informal description

Let $f : \beta \to \alpha$ be a function and $s$ a subset of $\beta$. If the image $f(s)$ is bounded above in $\alpha$, then for any element $c \in s$, we have $f(c) \leq \sup_{i \in s} f(i)$.

ciInf_mono theorem

{f g : ι → α} (B : BddBelow (range f)) (H : ∀ x, f x ≤ g x) : iInf f ≤ iInf g

Full source

/-- The indexed infimum of two functions are comparable if the functions are pointwise comparable -/
theorem ciInf_mono {f g : ι → α} (B : BddBelow (range f)) (H : ∀ x, f x ≤ g x) : iInf f ≤ iInf g :=
  ciSup_mono (α := αᵒᵈ) B H

Monotonicity of Indexed Infimum in Conditionally Complete Lattices

Informal description

Let $\iota$ be a type and $\alpha$ a conditionally complete lattice. Given two functions $f, g : \iota \to \alpha$ such that the range of $f$ is bounded below and $f(x) \leq g(x)$ for all $x \in \iota$, the indexed infimum satisfies $\bigsqcap_{i \in \iota} f(i) \leq \bigsqcap_{i \in \iota} g(i)$.

le_ciInf theorem

[Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, c ≤ f x) : c ≤ iInf f

Full source

/-- The indexed minimum of a function is bounded below by a uniform lower bound -/
theorem le_ciInf [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, c ≤ f x) : c ≤ iInf f :=
  ciSup_le (α := αᵒᵈ) H

Uniform Lower Bound for Indexed Infimum

Informal description

Let $\iota$ be a nonempty type and $f : \iota \to \alpha$ be a function into a conditionally complete lattice $\alpha$. If there exists an element $c \in \alpha$ such that $c \leq f(x)$ for all $x \in \iota$, then $c \leq \bigsqcap_{i \in \iota} f(i)$.

ciInf_le theorem

{f : ι → α} (H : BddBelow (range f)) (c : ι) : iInf f ≤ f c

Full source

/-- The indexed infimum of a function is bounded above by the value taken at one point -/
theorem ciInf_le {f : ι → α} (H : BddBelow (range f)) (c : ι) : iInf f ≤ f c :=
  le_ciSup (α := αᵒᵈ) H c

Indexed Infimum is Bounded Below by Function Value

Informal description

Let $f : \iota \to \alpha$ be a function from a type $\iota$ to a conditionally complete lattice $\alpha$. If the range of $f$ is bounded below, then for any $c \in \iota$, the infimum of $f$ is less than or equal to the value $f(c)$, i.e., $\inf f \leq f(c)$.

ciInf_le_of_le theorem

{f : ι → α} (H : BddBelow (range f)) (c : ι) (h : f c ≤ a) : iInf f ≤ a

Full source

theorem ciInf_le_of_le {f : ι → α} (H : BddBelow (range f)) (c : ι) (h : f c ≤ a) : iInf f ≤ a :=
  le_ciSup_of_le (α := αᵒᵈ) H c h

Infimum Bound via Element-wise Comparison: $\inf f \leq a$ when $f(c) \leq a$ for some $c$

Informal description

Let $f : \iota \to \alpha$ be a function from a type $\iota$ to a conditionally complete lattice $\alpha$, and suppose the range of $f$ is bounded below. For any element $a \in \alpha$ and index $c \in \iota$, if $f(c) \leq a$, then $\inf f \leq a$.

ciInf_set_le theorem

{f : β → α} {s : Set β} (H : BddBelow (f '' s)) {c : β} (hc : c ∈ s) : ⨅ i : s, f i ≤ f c

Full source

theorem ciInf_set_le {f : β → α} {s : Set β} (H : BddBelow (f '' s)) {c : β} (hc : c ∈ s) :
    ⨅ i : s, f i ≤ f c :=
  le_ciSup_set (α := αᵒᵈ) H hc

Element-wise lower bound for infimum over a set

Informal description

Let $f : \beta \to \alpha$ be a function and $s$ a subset of $\beta$. If the image $f(s)$ is bounded below in $\alpha$, then for any element $c \in s$, we have $\inf_{i \in s} f(i) \leq f(c)$.

ciInf_le_ciSup theorem

[Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) (hf' : BddAbove (range f)) : ⨅ i, f i ≤ ⨆ i, f i

Full source

lemma ciInf_le_ciSup [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) (hf' : BddAbove (range f)) :
    ⨅ i, f i ≤ ⨆ i, f i :=
  (ciInf_le hf (Classical.arbitrary _)).trans <| le_ciSup hf' (Classical.arbitrary _)

Infimum Bounded by Supremum in Conditionally Complete Lattices

Informal description

Let $\iota$ be a nonempty type and $f : \iota \to \alpha$ a function from $\iota$ to a conditionally complete lattice $\alpha$. If the range of $f$ is both bounded below and bounded above, then the infimum of $f$ is less than or equal to its supremum, i.e., $\inf_{i \in \iota} f(i) \leq \sup_{i \in \iota} f(i)$.

ciSup_const theorem

[hι : Nonempty ι] {a : α} : ⨆ _ : ι, a = a

Full source

@[simp]
theorem ciSup_const [hι : Nonempty ι] {a : α} : ⨆ _ : ι, a = a := by
  rw [iSup, range_const, csSup_singleton]

Supremum of a Constant Function in a Conditionally Complete Lattice

Informal description

For any nonempty type $\iota$ and any element $a$ in a conditionally complete lattice $\alpha$, the supremum of the constant function $f(i) = a$ over $\iota$ is equal to $a$, i.e., $\bigsqcup_{i \in \iota} a = a$.

ciInf_const theorem

[Nonempty ι] {a : α} : ⨅ _ : ι, a = a

Full source

@[simp]
theorem ciInf_const [Nonempty ι] {a : α} : ⨅ _ : ι, a = a :=
  ciSup_const (α := αᵒᵈ)

Infimum of a Constant Function in a Conditionally Complete Lattice

Informal description

For any nonempty type $\iota$ and any element $a$ in a conditionally complete lattice $\alpha$, the infimum of the constant function $f(i) = a$ over $\iota$ is equal to $a$, i.e., $\bigsqcap_{i \in \iota} a = a$.

ciSup_unique theorem

[Unique ι] {s : ι → α} : ⨆ i, s i = s default

Full source

@[simp]
theorem ciSup_unique [Unique ι] {s : ι → α} : ⨆ i, s i = s default := by
  have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)
  simp only [this, ciSup_const]

Supremum of a Function over a Unique Type Equals its Value at Default

Informal description

For any unique type $\iota$ (i.e., a type with exactly one element) and any function $s : \iota \to \alpha$ where $\alpha$ is a conditionally complete lattice, the supremum of $s$ over $\iota$ is equal to the value of $s$ at the default element of $\iota$, i.e., $\bigsqcup_{i \in \iota} s(i) = s(\text{default})$.

ciInf_unique theorem

[Unique ι] {s : ι → α} : ⨅ i, s i = s default

Full source

@[simp]
theorem ciInf_unique [Unique ι] {s : ι → α} : ⨅ i, s i = s default :=
  ciSup_unique (α := αᵒᵈ)

Infimum of a Function over a Unique Type Equals its Value at Default

Informal description

For any unique type $\iota$ (i.e., a type with exactly one element) and any function $s : \iota \to \alpha$ where $\alpha$ is a conditionally complete lattice, the infimum of $s$ over $\iota$ is equal to the value of $s$ at the default element of $\iota$, i.e., $\bigsqcap_{i \in \iota} s(i) = s(\text{default})$.

ciSup_subsingleton theorem

[Subsingleton ι] (i : ι) (s : ι → α) : ⨆ i, s i = s i

Full source

theorem ciSup_subsingleton [Subsingleton ι] (i : ι) (s : ι → α) : ⨆ i, s i = s i :=
  @ciSup_unique α ι _ ⟨⟨i⟩, fun j => Subsingleton.elim j i⟩ _

Supremum over a Subsingleton Type Equals Function Value

Informal description

For any subsingleton type $\iota$ (i.e., a type with at most one element) and any function $s : \iota \to \alpha$ where $\alpha$ is a conditionally complete lattice, the supremum of $s$ over $\iota$ is equal to $s(i)$ for any element $i \in \iota$, i.e., $\bigsqcup_{i \in \iota} s(i) = s(i)$.

ciInf_subsingleton theorem

[Subsingleton ι] (i : ι) (s : ι → α) : ⨅ i, s i = s i

Full source

theorem ciInf_subsingleton [Subsingleton ι] (i : ι) (s : ι → α) : ⨅ i, s i = s i :=
  @ciInf_unique α ι _ ⟨⟨i⟩, fun j => Subsingleton.elim j i⟩ _

Infimum over Subsingleton Type Equals Function Value

Informal description

For any subsingleton type $\iota$ (i.e., a type with at most one element) and any function $s : \iota \to \alpha$ where $\alpha$ is a conditionally complete lattice, the infimum of $s$ over $\iota$ is equal to $s(i)$ for any element $i \in \iota$, i.e., $\bigsqcap_{i \in \iota} s(i) = s(i)$.

ciSup_pos theorem

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

Full source

@[simp]
theorem ciSup_pos {p : Prop} {f : p → α} (hp : p) : ⨆ h : p, f h = f hp :=
  ciSup_subsingleton hp f

Supremum over True Proposition Equals Function Value

Informal description

For any proposition $p$ and any function $f : p \to \alpha$ where $\alpha$ is a conditionally complete lattice, if $p$ holds (i.e., $hp : p$), then the supremum of $f$ over $p$ is equal to $f(hp)$, i.e., \[ \bigsqcup_{h:p} f(h) = f(hp). \]

ciInf_pos theorem

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

Full source

@[simp]
theorem ciInf_pos {p : Prop} {f : p → α} (hp : p) : ⨅ h : p, f h = f hp :=
  ciSup_pos (α := αᵒᵈ) hp

Infimum over True Proposition Equals Function Value

Informal description

For any proposition $p$ and any function $f : p \to \alpha$ where $\alpha$ is a conditionally complete lattice, if $p$ holds (i.e., $hp : p$), then the infimum of $f$ over $p$ is equal to $f(hp)$, i.e., \[ \bigsqcap_{h:p} f(h) = f(hp). \]

ciSup_neg theorem

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

Full source

lemma ciSup_neg {p : Prop} {f : p → α} (hp : ¬ p) :
    ⨆ (h : p), f h = sSup (∅ : Set α) := by
  rw [iSup]
  congr
  rwa [range_eq_empty_iff, isEmpty_Prop]

Supremum over False Proposition Equals Supremum of Empty Set

Informal description

For any proposition $p$ and function $f : p \to \alpha$ where $\alpha$ is a conditionally complete lattice, if $p$ is false (i.e., $\neg p$ holds), then the supremum of $f$ over $p$ equals the supremum of the empty set in $\alpha$, i.e., \[ \bigsqcup_{h:p} f(h) = \sup(\emptyset). \]

ciInf_neg theorem

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

Full source

lemma ciInf_neg {p : Prop} {f : p → α} (hp : ¬ p) :
    ⨅ (h : p), f h = sInf (∅ : Set α) :=
  ciSup_neg (α := αᵒᵈ) hp

Infimum over False Proposition Equals Infimum of Empty Set

Informal description

For any proposition $p$ and function $f : p \to \alpha$ where $\alpha$ is a conditionally complete lattice, if $p$ is false (i.e., $\neg p$ holds), then the infimum of $f$ over $p$ equals the infimum of the empty set in $\alpha$, i.e., \[ \bigsqcap_{h:p} f(h) = \inf(\emptyset). \]

ciSup_eq_ite theorem

{p : Prop} [Decidable p] {f : p → α} : (⨆ h : p, f h) = if h : p then f h else sSup (∅ : Set α)

Full source

lemma ciSup_eq_ite {p : Prop} [Decidable p] {f : p → α} :
    (⨆ h : p, f h) = if h : p then f h else sSup (∅ : Set α) := by
  by_cases H : p <;> simp [ciSup_neg, H]

Conditional Supremum as If-Then-Else Expression

Informal description

For any proposition $p$ with a decidable instance, and any function $f : p \to \alpha$ where $\alpha$ is a conditionally complete lattice, the supremum of $f$ over $p$ is equal to $f(h)$ if $p$ holds (with witness $h$), and otherwise equals the supremum of the empty set, i.e., \[ \bigsqcup_{h:p} f(h) = \begin{cases} f(h) & \text{if } p \text{ holds} \\ \sup(\emptyset) & \text{otherwise.} \end{cases} \]

ciInf_eq_ite theorem

{p : Prop} [Decidable p] {f : p → α} : (⨅ h : p, f h) = if h : p then f h else sInf (∅ : Set α)

Full source

lemma ciInf_eq_ite {p : Prop} [Decidable p] {f : p → α} :
    (⨅ h : p, f h) = if h : p then f h else sInf (∅ : Set α) :=
  ciSup_eq_ite (α := αᵒᵈ)

Conditional Infimum as If-Then-Else Expression

Informal description

For any proposition $p$ with a decidable instance, and any function $f : p \to \alpha$ where $\alpha$ is a conditionally complete lattice, the infimum of $f$ over $p$ is equal to $f(h)$ if $p$ holds (with witness $h$), and otherwise equals the infimum of the empty set, i.e., \[ \bigsqcap_{h:p} f(h) = \begin{cases} f(h) & \text{if } p \text{ holds} \\ \inf(\emptyset) & \text{otherwise.} \end{cases} \]

cbiSup_eq_of_forall theorem

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

Full source

theorem cbiSup_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i, p i) :
    ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f := by
  simp only [hp, ciSup_unique]
  simp only [iSup]
  congr
  apply Subset.antisymm
  · rintro - ⟨i, rfl⟩
    simp [hp i]
  · rintro - ⟨i, rfl⟩
    simp

Supremum Equality for Universally Satisfied Predicates in Conditionally Complete Lattices

Informal description

For any conditionally complete lattice $\alpha$, any index type $\iota$, and any predicate $p : \iota \to \text{Prop}$ such that $p(i)$ holds for all $i \in \iota$, the supremum of a function $f$ over the subtype $\{i \in \iota \mid p(i)\}$ is equal to the supremum of $f$ over all indices, i.e., \[ \bigsqcup_{i \in \iota} \bigsqcup_{h : p(i)} f(\langle i, h \rangle) = \bigsqcup f. \]

cbiInf_eq_of_forall theorem

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

Full source

theorem cbiInf_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i, p i) :
    ⨅ (i) (h : p i), f ⟨i, h⟩ = iInf f :=
  cbiSup_eq_of_forall (α := αᵒᵈ) hp

Infimum Equality for Universally Satisfied Predicates in Conditionally Complete Lattices

Informal description

For any conditionally complete lattice $\alpha$, any index type $\iota$, and any predicate $p : \iota \to \text{Prop}$ such that $p(i)$ holds for all $i \in \iota$, the infimum of a function $f$ over the subtype $\{i \in \iota \mid p(i)\}$ is equal to the infimum of $f$ over all indices, i.e., \[ \bigsqcap_{i \in \iota} \bigsqcap_{h : p(i)} f(\langle i, h \rangle) = \bigsqcap f. \]

ciSup_eq_of_forall_le_of_forall_lt_exists_gt theorem

[Nonempty ι] {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 `iSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
theorem ciSup_eq_of_forall_le_of_forall_lt_exists_gt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, f i ≤ b)
    (h₂ : ∀ w, w < b → ∃ i, w < f i) : ⨆ i : ι, f i = b :=
  csSup_eq_of_forall_le_of_forall_lt_exists_gt (range_nonempty f) (forall_mem_range.mpr h₁)
    fun w hw => exists_range_iff.mpr <| h₂ w hw

Characterization of Supremum in Conditionally Complete Lattices

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of elements in a conditionally complete lattice $\alpha$, where $\iota$ is nonempty. 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 family equals $b$, i.e., $\sup_{i \in \iota} f_i = b$.

ciInf_eq_of_forall_ge_of_forall_gt_exists_lt theorem

[Nonempty ι] {f : ι → α} (h₁ : ∀ i, b ≤ f i) (h₂ : ∀ 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 `iInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/
theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, b ≤ f i)
    (h₂ : ∀ w, b < w → ∃ i, f i < w) : ⨅ i : ι, f i = b :=
  ciSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ) h₁ h₂

Characterization of Infimum in Conditionally Complete Lattices

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of elements in a conditionally complete lattice $\alpha$, where $\iota$ is nonempty. 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 family equals $b$, i.e., $\inf_{i \in \iota} f_i = b$.

Monotone.ciSup_mem_iInter_Icc_of_antitone theorem

 [SemilatticeSup β] {f g : β → α} (hf : Monotone f) (hg : Antitone g) (h : f ≤ g) : (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n)

Full source

/-- **Nested intervals lemma**: if `f` is a monotone sequence, `g` is an antitone sequence, and
`f n ≤ g n` for all `n`, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
theorem Monotone.ciSup_mem_iInter_Icc_of_antitone [SemilatticeSup β] {f g : β → α} (hf : Monotone f)
    (hg : Antitone g) (h : f ≤ g) : (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) := by
  refine mem_iInter.2 fun n => ?_
  haveI : Nonempty β := ⟨n⟩
  have : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n
  exact ⟨le_ciSup ⟨g <| n, forall_mem_range.2 this⟩ _, ciSup_le this⟩

Nested Intervals Property for Monotone and Antitone Sequences

Informal description

Let $\beta$ be a semilattice with a supremum operation, and let $\alpha$ be a conditionally complete lattice. Given two functions $f, g : \beta \to \alpha$ such that: 1. $f$ is monotone, 2. $g$ is antitone, 3. $f(n) \leq g(n)$ for all $n \in \beta$, then the supremum $\bigsqcup_{n \in \beta} f(n)$ belongs to the intersection of all closed intervals $[f(n), g(n)]$ for $n \in \beta$.

ciSup_mem_iInter_Icc_of_antitone_Icc theorem

 [SemilatticeSup β] {f g : β → α} (h : Antitone fun n => Icc (f n) (g n)) (h' : ∀ n, f n ≤ g n) :
  (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n)

Full source

/-- Nested intervals lemma: if `[f n, g n]` is an antitone sequence of nonempty
closed intervals, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`. -/
theorem ciSup_mem_iInter_Icc_of_antitone_Icc [SemilatticeSup β] {f g : β → α}
    (h : Antitone fun n => Icc (f n) (g n)) (h' : ∀ n, f n ≤ g n) :
    (⨆ n, f n) ∈ ⋂ n, Icc (f n) (g n) :=
  Monotone.ciSup_mem_iInter_Icc_of_antitone
    (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).1)
    (fun _ n hmn => ((Icc_subset_Icc_iff (h' n)).1 (h hmn)).2) h'

Nested Intervals Property for Antitone Interval Sequences

Informal description

Let $\beta$ be a semilattice with a supremum operation, and let $\alpha$ be a conditionally complete lattice. Given two functions $f, g : \beta \to \alpha$ such that: 1. The sequence of closed intervals $[f(n), g(n)]$ is antitone (i.e., $[f(n+1), g(n+1)] \subseteq [f(n), g(n)]$ for all $n$), 2. $f(n) \leq g(n)$ for all $n \in \beta$, then the supremum $\bigsqcup_{n \in \beta} f(n)$ belongs to the intersection of all closed intervals $[f(n), g(n)]$ for $n \in \beta$.

Set.Iic_ciInf theorem

[Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) : Iic (⨅ i, f i) = ⋂ i, Iic (f i)

Full source

lemma Set.Iic_ciInf [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) :
    Iic (⨅ i, f i) = ⋂ i, Iic (f i) := by
  apply Subset.antisymm
  · rintro x hx - ⟨i, rfl⟩
    exact hx.trans (ciInf_le hf _)
  · rintro x hx
    apply le_ciInf
    simpa using hx

Lower Closure of Infimum Equals Intersection of Lower Closures

Informal description

Let $\iota$ be a nonempty type and $f : \iota \to \alpha$ be a function into a conditionally complete lattice $\alpha$. If the range of $f$ is bounded below, then the lower closure of the infimum of $f$ equals the intersection of the lower closures of its values, i.e., \[ \{x \in \alpha \mid x \leq \inf f\} = \bigcap_{i \in \iota} \{x \in \alpha \mid x \leq f(i)\}. \]

Set.Ici_ciSup theorem

[Nonempty ι] {f : ι → α} (hf : BddAbove (range f)) : Ici (⨆ i, f i) = ⋂ i, Ici (f i)

Full source

lemma Set.Ici_ciSup [Nonempty ι] {f : ι → α} (hf : BddAbove (range f)) :
    Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
  Iic_ciInf (α := αᵒᵈ) hf

Upper Closure of Supremum Equals Intersection of Upper Closures

Informal description

Let $\iota$ be a nonempty type and $f : \iota \to \alpha$ be a function into a conditionally complete lattice $\alpha$. If the range of $f$ is bounded above, then the upper closure of the supremum of $f$ equals the intersection of the upper closures of its values, i.e., \[ \{x \in \alpha \mid x \geq \sup f\} = \bigcap_{i \in \iota} \{x \in \alpha \mid x \geq f(i)\}. \]

ciSup_subtype theorem

 [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α} (hf : BddAbove (Set.range f))
  (hf' : sSup ∅ ≤ iSup f) : iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩

Full source

theorem ciSup_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α}
    (hf : BddAbove (Set.range f)) (hf' : sSup ∅ ≤ iSup f) :
    iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ := by
  classical
  refine le_antisymm (ciSup_le ?_) ?_
  · intro ⟨i, h⟩
    have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]
    rw [this]
    refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i
    simp_rw [ciSup_eq_ite]
    refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_
    intro
    simp only [Set.mem_range, Set.union_singleton, Set.mem_insert_iff, Subtype.exists,
      forall_exists_index]
    intro b hb
    split_ifs at hb
    · exact Or.inr ⟨_, _, hb⟩
    · simp_all
  · refine ciSup_le fun i ↦ ?_
    simp_rw [ciSup_eq_ite]
    split_ifs
    · exact le_ciSup hf ?_
    · exact hf'

Supremum of Subtype Function Equals Indexed Supremum

Informal description

Let $\iota$ be a nonempty type, $p : \iota \to \text{Prop}$ a predicate on $\iota$, and $f : \{i \in \iota \mid p(i)\} \to \alpha$ a function into a conditionally complete lattice $\alpha$. Assume the range of $f$ is bounded above and that the supremum of the empty set is less than or equal to the supremum of $f$. Then the supremum of $f$ equals the supremum over all $i \in \iota$ and $h : p(i)$ of $f(\langle i, h\rangle)$, i.e., \[ \sup f = \sup_{i \in \iota, h : p(i)} f(\langle i, h\rangle). \]

ciInf_subtype theorem

 [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α} (hf : BddBelow (Set.range f))
  (hf' : iInf f ≤ sInf ∅) : iInf f = ⨅ (i) (h : p i), f ⟨i, h⟩

Full source

theorem ciInf_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α}
    (hf : BddBelow (Set.range f)) (hf' : iInf f ≤ sInf ∅) :
    iInf f = ⨅ (i) (h : p i), f ⟨i, h⟩ :=
  ciSup_subtype (α := αᵒᵈ) hf hf'

Infimum of Subtype Function Equals Indexed Infimum

Informal description

Let $\iota$ be a nonempty type, $p : \iota \to \text{Prop}$ a predicate on $\iota$, and $f : \{i \in \iota \mid p(i)\} \to \alpha$ a function into a conditionally complete lattice $\alpha$. Assume the range of $f$ is bounded below and that the infimum of $f$ is less than or equal to the infimum of the empty set. Then the infimum of $f$ equals the infimum over all $i \in \iota$ and $h : p(i)$ of $f(\langle i, h\rangle)$, i.e., \[ \inf f = \inf_{i \in \iota, h : p(i)} f(\langle i, h\rangle). \]

ciSup_subtype' theorem

 [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : ∀ i, p i → α}
  (hf : BddAbove (Set.range (fun i : Subtype p ↦ f i i.prop))) (hf' : sSup ∅ ≤ ⨆ (i : Subtype p), f i i.prop) :
  ⨆ (i) (h), f i h = ⨆ x : Subtype p, f x x.property

Full source

theorem ciSup_subtype' [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : ∀ i, p i → α}
    (hf : BddAbove (Set.range (fun i : Subtype p ↦ f i i.prop)))
    (hf' : sSup ∅ ≤ ⨆ (i : Subtype p), f i i.prop) :
    ⨆ (i) (h), f i h = ⨆ x : Subtype p, f x x.property :=
  (ciSup_subtype (f := fun x => f x.val x.property) hf hf').symm

Supremum Equality for Subtype Functions in Conditionally Complete Lattices

Informal description

Let $\iota$ be a nonempty type, $p : \iota \to \text{Prop}$ a predicate on $\iota$, and $f : \forall i, p(i) \to \alpha$ a function into a conditionally complete lattice $\alpha$. Assume the range of $\lambda (i : \{i \mid p(i)\}), f(i, i.\text{prop})$ is bounded above and that the supremum of the empty set is less than or equal to the supremum of $f$ over its subtype. Then the supremum over all $i \in \iota$ and $h : p(i)$ of $f(i, h)$ equals the supremum over all $x$ in the subtype $\{i \mid p(i)\}$ of $f(x, x.\text{prop})$, i.e., \[ \sup_{i, h} f(i, h) = \sup_{x \in \{i \mid p(i)\}} f(x, x.\text{prop}). \]

ciInf_subtype' theorem

 [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : ∀ i, p i → α}
  (hf : BddBelow (Set.range (fun i : Subtype p ↦ f i i.prop))) (hf' : ⨅ (i : Subtype p), f i i.prop ≤ sInf ∅) :
  ⨅ (i) (h), f i h = ⨅ x : Subtype p, f x x.property

Full source

theorem ciInf_subtype' [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : ∀ i, p i → α}
    (hf : BddBelow (Set.range (fun i : Subtype p ↦ f i i.prop)))
    (hf' : ⨅ (i : Subtype p), f i i.prop ≤ sInf ∅) :
    ⨅ (i) (h), f i h = ⨅ x : Subtype p, f x x.property :=
  (ciInf_subtype (f := fun x => f x.val x.property) hf hf').symm

Infimum Equality for Subtype Functions in Conditionally Complete Lattices

Informal description

Let $\iota$ be a nonempty type, $p : \iota \to \text{Prop}$ a predicate on $\iota$, and $f : \forall i, p(i) \to \alpha$ a function into a conditionally complete lattice $\alpha$. Assume the range of $\lambda (i : \{i \mid p(i)\}), f(i, i.\text{prop})$ is bounded below and that the infimum of $f$ over its subtype is less than or equal to the infimum of the empty set. Then the infimum over all $i \in \iota$ and $h : p(i)$ of $f(i, h)$ equals the infimum over all $x$ in the subtype $\{i \mid p(i)\}$ of $f(x, x.\text{prop})$, i.e., \[ \inf_{i, h} f(i, h) = \inf_{x \in \{i \mid p(i)\}} f(x, x.\text{prop}). \]

ciSup_subtype'' theorem

 {ι} [Nonempty ι] {s : Set ι} (hs : s.Nonempty) {f : ι → α} (hf : BddAbove (Set.range fun i : s ↦ f i))
  (hf' : sSup ∅ ≤ ⨆ i : s, f i) : ⨆ i : s, f i = ⨆ (t : ι) (_ : t ∈ s), f t

Full source

theorem ciSup_subtype'' {ι} [Nonempty ι] {s : Set ι} (hs : s.Nonempty) {f : ι → α}
    (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) :
    ⨆ i : s, f i = ⨆ (t : ι) (_ : t ∈ s), f t :=
  haveI : Nonempty s := Set.Nonempty.to_subtype hs
  ciSup_subtype hf hf'

Supremum Equality for Restricted Function in Conditionally Complete Lattice

Informal description

Let $\iota$ be a nonempty type, $s \subseteq \iota$ a nonempty subset, and $f : \iota \to \alpha$ a function into a conditionally complete lattice $\alpha$. If the range of $f$ restricted to $s$ is bounded above and the supremum of the empty set is less than or equal to the supremum of $f$ over $s$, then the supremum of $f$ over $s$ equals the supremum over all $t \in s$ of $f(t)$, i.e., \[ \sup_{i \in s} f(i) = \sup_{t \in s} f(t). \]

ciInf_subtype'' theorem

 {ι} [Nonempty ι] {s : Set ι} (hs : s.Nonempty) {f : ι → α} (hf : BddBelow (Set.range fun i : s ↦ f i))
  (hf' : ⨅ i : s, f i ≤ sInf ∅) : ⨅ i : s, f i = ⨅ (t : ι) (_ : t ∈ s), f t

Full source

theorem ciInf_subtype'' {ι} [Nonempty ι] {s : Set ι} (hs : s.Nonempty) {f : ι → α}
    (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) :
    ⨅ i : s, f i = ⨅ (t : ι) (_ : t ∈ s), f t :=
  haveI : Nonempty s := Set.Nonempty.to_subtype hs
  ciInf_subtype hf hf'

Infimum Equality for Restricted Function in Conditionally Complete Lattice

Informal description

Let $\iota$ be a nonempty type, $s \subseteq \iota$ a nonempty subset, and $f : \iota \to \alpha$ a function into a conditionally complete lattice $\alpha$. If the range of $f$ restricted to $s$ is bounded below and the infimum of $f$ over $s$ is less than or equal to the infimum of the empty set, then the infimum of $f$ over $s$ equals the infimum over all $t \in s$ of $f(t)$, i.e., \[ \inf_{i \in s} f(i) = \inf_{t \in s} f(t). \]

csSup_image theorem

 [Nonempty β] {s : Set β} (hs : s.Nonempty) {f : β → α} (hf : BddAbove (Set.range fun i : s ↦ f i))
  (hf' : sSup ∅ ≤ ⨆ i : s, f i) : sSup (f '' s) = ⨆ a ∈ s, f a

Full source

theorem csSup_image [Nonempty β] {s : Set β} (hs : s.Nonempty) {f : β → α}
    (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) :
    sSup (f '' s) = ⨆ a ∈ s, f a := by
  rw [← ciSup_subtype'' hs hf hf', iSup, Set.image_eq_range]

Supremum of Image Equals Supremum over Set in Conditionally Complete Lattice

Informal description

Let $\beta$ be a nonempty type and $s \subseteq \beta$ a nonempty subset. Given a function $f : \beta \to \alpha$ into a conditionally complete lattice $\alpha$, if the range of $f$ restricted to $s$ is bounded above and the supremum of the empty set is less than or equal to the supremum of $f$ over $s$, then the supremum of the image of $s$ under $f$ equals the supremum of $f$ over $s$, i.e., \[ \sup(f(s)) = \sup_{a \in s} f(a). \]

csInf_image theorem

 [Nonempty β] {s : Set β} (hs : s.Nonempty) {f : β → α} (hf : BddBelow (Set.range fun i : s ↦ f i))
  (hf' : ⨅ i : s, f i ≤ sInf ∅) : sInf (f '' s) = ⨅ a ∈ s, f a

Full source

theorem csInf_image [Nonempty β] {s : Set β} (hs : s.Nonempty) {f : β → α}
    (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) :
    sInf (f '' s) = ⨅ a ∈ s, f a :=
  csSup_image (α := αᵒᵈ) hs hf hf'

Infimum of Image Equals Infimum over Set in Conditionally Complete Lattice

Informal description

Let $\beta$ be a nonempty type and $s \subseteq \beta$ a nonempty subset. Given a function $f : \beta \to \alpha$ into a conditionally complete lattice $\alpha$, if the range of $f$ restricted to $s$ is bounded below and the infimum of $f$ over $s$ is less than or equal to the infimum of the empty set, then the infimum of the image of $s$ under $f$ equals the infimum of $f$ over $s$, i.e., \[ \inf(f(s)) = \inf_{a \in s} f(a). \]

ciSup_image theorem

 {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι'] {s : Set ι} (hs : s.Nonempty) {f : ι → ι'}
  {g : ι' → α} (hf : BddAbove (Set.range fun i : s ↦ g (f i))) (hg' : sSup ∅ ≤ ⨆ i : s, g (f i)) :
  ⨆ i ∈ (f '' s), g i = ⨆ x ∈ s, g (f x)

Full source

lemma ciSup_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι']
    {s : Set ι} (hs : s.Nonempty) {f : ι → ι'} {g : ι' → α}
    (hf : BddAbove (Set.range fun i : s ↦ g (f i))) (hg' : sSup ∅ ≤ ⨆ i : s, g (f i)) :
    ⨆ i ∈ (f '' s), g i = ⨆ x ∈ s, g (f x) := by
  have hg : BddAbove (Set.range fun i : f '' s ↦ g i) := by
    simpa [bddAbove_def] using hf
  have hf' : sSup ∅ ≤ ⨆ i : f '' s, g i := by
    refine hg'.trans ?_
    have : Nonempty s := Set.Nonempty.to_subtype hs
    refine ciSup_le ?_
    intro ⟨i, h⟩
    obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) := by
      have : f i ∈ f '' s := Set.mem_image_of_mem _ h
      exact ⟨⟨f i, this⟩, by simp [this]⟩
    rw [← ht]
    refine le_ciSup_set ?_ t.prop
    simpa [bddAbove_def] using hf
  rw [← csSup_image (by simpa using hs) hg hf', ← csSup_image hs hf hg', ← Set.image_comp, comp_def]

Equality of Indexed Suprema under Function Image in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $\iota$ and $\iota'$ be nonempty types. Given a nonempty subset $s \subseteq \iota$, a function $f \colon \iota \to \iota'$, and a function $g \colon \iota' \to \alpha$, if the range of $g \circ f$ restricted to $s$ is bounded above and the supremum of the empty set is less than or equal to the supremum of $g \circ f$ over $s$, then the indexed supremum of $g$ over the image $f(s)$ equals the indexed supremum of $g \circ f$ over $s$, i.e., \[ \bigsqcup_{i \in f(s)} g(i) = \bigsqcup_{x \in s} g(f(x)). \]

ciInf_image theorem

 {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι'] {s : Set ι} (hs : s.Nonempty) {f : ι → ι'}
  {g : ι' → α} (hf : BddBelow (Set.range fun i : s ↦ g (f i))) (hg' : ⨅ i : s, g (f i) ≤ sInf ∅) :
  ⨅ i ∈ (f '' s), g i = ⨅ x ∈ s, g (f x)

Full source

lemma ciInf_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι']
    {s : Set ι} (hs : s.Nonempty) {f : ι → ι'} {g : ι' → α}
    (hf : BddBelow (Set.range fun i : s ↦ g (f i))) (hg' : ⨅ i : s, g (f i) ≤ sInf ∅) :
    ⨅ i ∈ (f '' s), g i = ⨅ x ∈ s, g (f x) :=
  ciSup_image (α := αᵒᵈ) hs hf hg'

Equality of Indexed Infima under Function Image in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $\iota$ and $\iota'$ be nonempty types. Given a nonempty subset $s \subseteq \iota$, a function $f \colon \iota \to \iota'$, and a function $g \colon \iota' \to \alpha$, if the range of $g \circ f$ restricted to $s$ is bounded below and the infimum of $g \circ f$ over $s$ is less than or equal to the infimum of the empty set, then the indexed infimum of $g$ over the image $f(s)$ equals the indexed infimum of $g \circ f$ over $s$, i.e., \[ \bigsqcap_{i \in f(s)} g(i) = \bigsqcap_{x \in s} g(f(x)). \]

exists_lt_of_lt_ciSup theorem

[Nonempty ι] {f : ι → α} (h : b < iSup f) : ∃ i, b < f i

Full source

/-- Indexed version of `exists_lt_of_lt_csSup`.
When `b < iSup f`, there is an element `i` such that `b < f i`.
-/
theorem exists_lt_of_lt_ciSup [Nonempty ι] {f : ι → α} (h : b < iSup f) : ∃ i, b < f i :=
  let ⟨_, ⟨i, rfl⟩, h⟩ := exists_lt_of_lt_csSup (range_nonempty f) h
  ⟨i, h⟩

Existence of Element Below Supremum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $\iota$ a nonempty type. For any function $f \colon \iota \to \alpha$ and any element $b \in \alpha$, if $b$ is strictly less than the supremum $\bigsqcup_{i \in \iota} f(i)$, then there exists an index $i \in \iota$ such that $b < f(i)$.

exists_lt_of_ciInf_lt theorem

[Nonempty ι] {f : ι → α} (h : iInf f < a) : ∃ i, f i < a

Full source

/-- Indexed version of `exists_lt_of_csInf_lt`.
When `iInf f < a`, there is an element `i` such that `f i < a`.
-/
theorem exists_lt_of_ciInf_lt [Nonempty ι] {f : ι → α} (h : iInf f < a) : ∃ i, f i < a :=
  exists_lt_of_lt_ciSup (α := αᵒᵈ) h

Existence of Element Below Infimum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $\iota$ a nonempty type. For any function $f \colon \iota \to \alpha$ and any element $a \in \alpha$, if the infimum $\bigsqcap_{i \in \iota} f(i)$ is strictly less than $a$, then there exists an index $i \in \iota$ such that $f(i) < a$.

lt_ciSup_iff theorem

[Nonempty ι] {f : ι → α} (hb : BddAbove (range f)) : a < iSup f ↔ ∃ i, a < f i

Full source

theorem lt_ciSup_iff [Nonempty ι] {f : ι → α} (hb : BddAbove (range f)) :
    a < iSup f ↔ ∃ i, a < f i := by
  simpa only [mem_range, exists_exists_eq_and] using lt_csSup_iff hb (range_nonempty _)

Characterization of Strict Supremum Inequality in Conditionally Complete Lattices

Informal description

Let $\iota$ be a nonempty type and $f : \iota \to \alpha$ be a function with bounded range in a conditionally complete lattice $\alpha$. For any element $a \in \alpha$, we have $a < \sup_i f(i)$ if and only if there exists some index $i \in \iota$ such that $a < f(i)$.

ciInf_lt_iff theorem

[Nonempty ι] {f : ι → α} (hb : BddBelow (range f)) : iInf f < a ↔ ∃ i, f i < a

Full source

theorem ciInf_lt_iff [Nonempty ι] {f : ι → α} (hb : BddBelow (range f)) :
    iInfiInf f < a ↔ ∃ i, f i < a := by
  simpa only [mem_range, exists_exists_eq_and] using csInf_lt_iff hb (range_nonempty _)

Infimum Less Than Criterion in Conditionally Complete Lattices

Informal description

Let $ι$ be a nonempty type and $f : ι \to α$ be a function into a conditionally complete linear order $α$. If the range of $f$ is bounded below, then the infimum of $f$ is less than a given element $a$ if and only if there exists some index $i$ such that $f(i) < a$. In symbols: \[ \inf_{i} f(i) < a \leftrightarrow \exists i, f(i) < a \]

cbiSup_eq_of_not_forall theorem

{p : ι → Prop} {f : Subtype p → α} (hp : ¬(∀ i, p i)) : ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f ⊔ sSup ∅

Full source

theorem cbiSup_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬ (∀ i, p i)) :
    ⨆ (i) (h : p i), f ⟨i, h⟩ = iSupiSup f ⊔ sSup ∅ := by
  classical
  rcases not_forall.1 hp with ⟨i₀, hi₀⟩
  have : Nonempty ι := ⟨i₀⟩
  simp only [ciSup_eq_ite]
  by_cases H : BddAbove (range f)
  · have B : BddAbove (range fun i ↦ if h : p i then f ⟨i, h⟩ else sSup ∅) := by
      rcases H with ⟨c, hc⟩
      refine ⟨c ⊔ sSup ∅, ?_⟩
      rintro - ⟨i, rfl⟩
      by_cases hi : p i
      · simp only [hi, dite_true, le_sup_iff, hc (mem_range_self _), true_or]
      · simp only [hi, dite_false, le_sup_right]
    apply le_antisymm
    · apply ciSup_le (fun i ↦ ?_)
      by_cases hi : p i
      · simp only [hi, dite_true, le_sup_iff]
        left
        exact le_ciSup H _
      · simp [hi]
    · apply sup_le
      · rcases isEmpty_or_nonempty (Subtype p) with hp|hp
        · rw [iSup_of_empty']
          convert le_ciSup B i₀
          simp [hi₀]
        · apply ciSup_le
          rintro ⟨i, hi⟩
          convert le_ciSup B i
          simp [hi]
      · convert le_ciSup B i₀
        simp [hi₀]
  · have : iSup f = sSup (∅ : Set α) := csSup_of_not_bddAbove H
    simp only [this, le_refl, sup_of_le_left]
    apply csSup_of_not_bddAbove
    contrapose! H
    apply H.mono
    rintro - ⟨i, rfl⟩
    convert mem_range_self i.1
    simp [i.2]

Supremum over Subtype with Non-Universal Predicate

Informal description

Let $\iota$ be a type and $p : \iota \to \text{Prop}$ be a predicate on $\iota$. For a function $f : \{i \in \iota \mid p(i)\} \to \alpha$ into a conditionally complete lattice $\alpha$, if there exists some $i \in \iota$ such that $\neg p(i)$, then the indexed supremum of $f$ over the subtype where $p$ holds equals the supremum of $f$ joined with the supremum of the empty set: \[ \bigsqcup_{i \in \iota, h : p(i)} f(\langle i, h \rangle) = \left(\bigsqcup f\right) \sqcup \sup(\emptyset). \]

cbiInf_eq_of_not_forall theorem

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

Full source

theorem cbiInf_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬ (∀ i, p i)) :
    ⨅ (i) (h : p i), f ⟨i, h⟩ = iInfiInf f ⊓ sInf ∅ :=
  cbiSup_eq_of_not_forall (α := αᵒᵈ) hp

Infimum over Subtype with Non-Universal Predicate

Informal description

Let $\iota$ be a type and $p : \iota \to \text{Prop}$ be a predicate on $\iota$. For a function $f : \{i \in \iota \mid p(i)\} \to \alpha$ into a conditionally complete lattice $\alpha$, if there exists some $i \in \iota$ such that $\neg p(i)$, then the indexed infimum of $f$ over the subtype where $p$ holds equals the infimum of $f$ meet with the infimum of the empty set: \[ \bigsqcap_{i \in \iota, h : p(i)} f(\langle i, h \rangle) = \left(\bigsqcap f\right) \sqcap \inf(\emptyset). \]

ciInf_eq_bot_of_bot_mem theorem

[OrderBot α] {f : ι → α} (hs : ⊥ ∈ range f) : iInf f = ⊥

Full source

theorem ciInf_eq_bot_of_bot_mem [OrderBot α] {f : ι → α} (hs : ⊥⊥ ∈ range f) : iInf f = ⊥ :=
  csInf_eq_bot_of_bot_mem hs

Infimum Equals Bottom When Bottom is in Range

Informal description

Let $\alpha$ be a conditionally complete lattice with a bottom element $\bot$. For any function $f : \iota \to \alpha$, if $\bot$ is in the range of $f$, then the infimum of $f$ over $\iota$ is equal to $\bot$, i.e., $\bigwedge_{i \in \iota} f(i) = \bot$.

ciInf_eq_top_of_top_mem theorem

[OrderTop α] {f : ι → α} (hs : ⊤ ∈ range f) : iSup f = ⊤

Full source

theorem ciInf_eq_top_of_top_mem [OrderTop α] {f : ι → α} (hs : ⊤⊤ ∈ range f) : iSup f = ⊤ :=
  csSup_eq_top_of_top_mem hs

Infimum Equals Top When Top is in Range

Informal description

Let $\alpha$ be a conditionally complete lattice with a top element $\top$, and let $f : \iota \to \alpha$ be a function such that $\top$ is in the range of $f$. Then the infimum of $f$ over $\iota$ is equal to $\top$, i.e., $\bigwedge_{i \in \iota} f(i) = \top$.

ciInf_mem theorem

[Nonempty ι] (f : ι → α) : iInf f ∈ range f

Full source

theorem ciInf_mem [Nonempty ι] (f : ι → α) : iInfiInf f ∈ range f :=
  csInf_mem (range_nonempty f)

Infimum of Nonempty Family Belongs to its Range

Informal description

Let $\alpha$ be a conditionally complete lattice and $\iota$ a nonempty type. For any function $f : \iota \to \alpha$, the infimum of $f$ over $\iota$ belongs to the range of $f$, i.e., $\bigwedge_{i \in \iota} f(i) \in \text{range}(f)$.

ciSup_of_empty theorem

[IsEmpty ι] (f : ι → α) : ⨆ i, f i = ⊥

Full source

@[simp]
theorem ciSup_of_empty [IsEmpty ι] (f : ι → α) : ⨆ i, f i = ⊥ := by
  rw [iSup_of_empty', csSup_empty]

Supremum over Empty Index Set Equals Bottom Element

Informal description

For any conditionally complete lattice with a bottom element $\bot$ and any function $f : \iota \to \alpha$ where the index type $\iota$ is empty, the supremum of $f$ over $\iota$ equals $\bot$, i.e., $\bigsqcup_{i \in \iota} f(i) = \bot$.

ciSup_false theorem

(f : False → α) : ⨆ i, f i = ⊥

Full source

theorem ciSup_false (f : False → α) : ⨆ i, f i = ⊥ :=
  ciSup_of_empty f

Supremum over False Equals Bottom Element

Informal description

For any conditionally complete lattice $\alpha$ with a bottom element $\bot$ and any function $f : \text{False} \to \alpha$, the supremum of $f$ over the empty type $\text{False}$ equals $\bot$, i.e., $\bigsqcup_{i \in \text{False}} f(i) = \bot$.

le_ciSup_iff' theorem

{s : ι → α} {a : α} (h : BddAbove (range s)) : a ≤ iSup s ↔ ∀ b, (∀ i, s i ≤ b) → a ≤ b

Full source

theorem le_ciSup_iff' {s : ι → α} {a : α} (h : BddAbove (range s)) :
    a ≤ iSup s ↔ ∀ b, (∀ i, s i ≤ b) → a ≤ b := by simp [iSup, h, le_csSup_iff', upperBounds]

Characterization of Supremum Bound in Conditionally Complete Lattices

Informal description

Let $α$ be a conditionally complete lattice, $s : ι → α$ be a function, and $a ∈ α$. If the range of $s$ is bounded above, then $a$ is less than or equal to the supremum of $s$ if and only if for every upper bound $b$ of $s$ (i.e., $s(i) ≤ b$ for all $i$), we have $a ≤ b$.

le_ciInf_iff' theorem

[Nonempty ι] {f : ι → α} {a : α} : a ≤ iInf f ↔ ∀ i, a ≤ f i

Full source

theorem le_ciInf_iff' [Nonempty ι] {f : ι → α} {a : α} : a ≤ iInf f ↔ ∀ i, a ≤ f i :=
  le_ciInf_iff (OrderBot.bddBelow _)

Characterization of Lower Bounds via Infimum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, $\iota$ be a nonempty type, and $f : \iota \to \alpha$ be a function. For any element $a \in \alpha$, we have $a \leq \inf_{i} f(i)$ if and only if $a \leq f(i)$ for all $i \in \iota$.

ciInf_le' theorem

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

Full source

theorem ciInf_le' (f : ι → α) (i : ι) : iInf f ≤ f i := ciInf_le (OrderBot.bddBelow _) _

Infimum is a Lower Bound for Function Values

Informal description

For any function $f : \iota \to \alpha$ from a type $\iota$ to a conditionally complete lattice $\alpha$, and for any index $i \in \iota$, the infimum of $f$ is less than or equal to $f(i)$, i.e., $\inf f \leq f(i)$.

ciInf_le_of_le' theorem

(c : ι) : f c ≤ a → iInf f ≤ a

Full source

lemma ciInf_le_of_le' (c : ι) : f c ≤ a → iInf f ≤ a := ciInf_le_of_le (OrderBot.bddBelow _) _

Infimum bound via element-wise comparison: $\inf f \leq a$ when $f(c) \leq a$ for some $c$

Informal description

For any function $f : \iota \to \alpha$ from a type $\iota$ to a conditionally complete lattice $\alpha$, and for any index $c \in \iota$, if $f(c) \leq a$ for some element $a \in \alpha$, then the infimum of $f$ satisfies $\inf f \leq a$.

ciSup_le_iff' theorem

{f : ι → α} (h : BddAbove (range f)) {a : α} : ⨆ i, f i ≤ a ↔ ∀ i, f i ≤ a

Full source

/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `ciSup_le_iff`. -/
theorem ciSup_le_iff' {f : ι → α} (h : BddAbove (range f)) {a : α} :
    ⨆ i, f i⨆ i, f i ≤ a ↔ ∀ i, f i ≤ a :=
  (csSup_le_iff' h).trans forall_mem_range

Characterization of Supremum Bound in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice with a bottom element, and let $f : \iota \to \alpha$ be a function whose range is bounded above. Then the supremum of $f$ is less than or equal to $a$ if and only if $f(i) \leq a$ for all $i \in \iota$. In symbols: \[ \bigsqcup_{i} f(i) \leq a \leftrightarrow \forall i, f(i) \leq a. \]

ciSup_le' theorem

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

Full source

theorem ciSup_le' {f : ι → α} {a : α} (h : ∀ i, f i ≤ a) : ⨆ i, f i ≤ a :=
  csSup_le' <| forall_mem_range.2 h

Supremum Bound in Conditionally Complete Lattices

Informal description

For a conditionally complete lattice $\alpha$ and a function $f : \iota \to \alpha$, if $f(i) \leq a$ for all $i \in \iota$, then the supremum of $f$ satisfies $\bigsqcup_{i} f(i) \leq a$.

lt_ciSup_iff' theorem

{f : ι → α} (h : BddAbove (range f)) : a < iSup f ↔ ∃ i, a < f i

Full source

/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `lt_ciSup_iff`. -/
theorem lt_ciSup_iff' {f : ι → α} (h : BddAbove (range f)) : a < iSup f ↔ ∃ i, a < f i := by
  simpa only [not_le, not_forall] using (ciSup_le_iff' h).not

Characterization of Strict Supremum Bound in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice with a bottom element, and let $f : \iota \to \alpha$ be a function whose range is bounded above. For any element $a \in \alpha$, we have $a < \bigsqcup_{i} f(i)$ if and only if there exists an index $i \in \iota$ such that $a < f(i)$. In symbols: \[ a < \bigsqcup_{i} f(i) \leftrightarrow \exists i, a < f(i). \]

exists_lt_of_lt_ciSup' theorem

{f : ι → α} {a : α} (h : a < ⨆ i, f i) : ∃ i, a < f i

Full source

theorem exists_lt_of_lt_ciSup' {f : ι → α} {a : α} (h : a < ⨆ i, f i) : ∃ i, a < f i := by
  contrapose! h
  exact ciSup_le' h

Existence of Element Exceeding Lower Bound in Conditionally Complete Lattices

Informal description

For a conditionally complete lattice $\alpha$ and a function $f : \iota \to \alpha$, if $a$ is strictly less than the supremum of $f$, then there exists an index $i \in \iota$ such that $a < f(i)$.

ciSup_mono' theorem

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

Full source

theorem ciSup_mono' {ι'} {f : ι → α} {g : ι' → α} (hg : BddAbove (range g))
    (h : ∀ i, ∃ i', f i ≤ g i') : iSup f ≤ iSup g :=
  ciSup_le' fun i => Exists.elim (h i) (le_ciSup_of_le hg)

Monotonicity of Supremum under Pointwise Comparison in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $f : \iota \to \alpha$ and $g : \iota' \to \alpha$ be two functions. If the range of $g$ is bounded above and for every $i \in \iota$ there exists $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'). \]

ciSup_or' theorem

(p q : Prop) (f : p ∨ q → α) : ⨆ (h : p ∨ q), f h = (⨆ h : p, f (.inl h)) ⊔ ⨆ h : q, f (.inr h)

Full source

lemma ciSup_or' (p q : Prop) (f : p ∨ q → α) :
    ⨆ (h : p ∨ q), f h = (⨆ h : p, f (.inl h)) ⊔ ⨆ h : q, f (.inr h) := by
  by_cases hp : p <;>
  by_cases hq : q <;>
  simp [hp, hq]

Supremum over Disjunction Equals Join of Suprema

Informal description

For any two propositions $p$ and $q$ and any function $f : p \lor q \to \alpha$ where $\alpha$ is a conditionally complete lattice, the supremum of $f$ over $p \lor q$ is equal to the join of the supremum of $f$ over $p$ and the supremum of $f$ over $q$, i.e., \[ \bigsqcup_{h \in p \lor q} f(h) = \left(\bigsqcup_{h \in p} f(\text{inl } h)\right) \sqcup \left(\bigsqcup_{h \in q} f(\text{inr } h)\right). \]

GaloisConnection.l_csSup theorem

(gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : l (sSup s) = ⨆ x : s, l x

Full source

theorem l_csSup (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
    l (sSup s) = ⨆ x : s, l x :=
  Eq.symm <| IsLUB.ciSup_set_eq (gc.isLUB_l_image <| isLUB_csSup hne hbdd) hne

Galois Connection Preserves Supremum for Nonempty Bounded Sets

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois connection (i.e., for all $x \in \alpha$ and $y \in \beta$, $l(x) \leq y \leftrightarrow x \leq u(y)$). For any nonempty subset $s \subseteq \alpha$ that is bounded above, the image of the supremum of $s$ under $l$ equals the indexed supremum of $l$ over $s$, i.e., $l(\sup s) = \bigsqcup_{x \in s} l(x)$.

GaloisConnection.l_csSup' theorem

(gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : l (sSup s) = sSup (l '' s)

Full source

theorem l_csSup' (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
    l (sSup s) = sSup (l '' s) := by rw [gc.l_csSup hne hbdd, sSup_image']

Galois Connection Preserves Supremum via Image of Set

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois connection (i.e., for all $x \in \alpha$ and $y \in \beta$, $l(x) \leq y \leftrightarrow x \leq u(y)$). For any nonempty subset $s \subseteq \alpha$ that is bounded above, the image of the supremum of $s$ under $l$ equals the supremum of the image of $s$ under $l$, i.e., $l(\sup s) = \sup (l \text{''} s)$.

GaloisConnection.l_ciSup theorem

(gc : GaloisConnection l u) {f : ι → α} (hf : BddAbove (range f)) : l (⨆ i, f i) = ⨆ i, l (f i)

Full source

theorem l_ciSup (gc : GaloisConnection l u) {f : ι → α} (hf : BddAbove (range f)) :
    l (⨆ i, f i) = ⨆ i, l (f i) := by rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']

Galois Connection Preserves Indexed Supremum for Bounded Functions

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois connection (i.e., for all $x \in \alpha$ and $y \in \beta$, $l(x) \leq y \leftrightarrow x \leq u(y)$). For any function $f : \iota \to \alpha$ whose range is bounded above, the image under $l$ of the indexed supremum of $f$ equals the indexed supremum of $l \circ f$, i.e., $l(\bigsqcup_{i} f(i)) = \bigsqcup_{i} l(f(i))$.

GaloisConnection.l_ciSup_set theorem

 (gc : GaloisConnection l u) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s)) (hne : s.Nonempty) :
  l (⨆ i : s, f i) = ⨆ i : s, l (f i)

Full source

theorem l_ciSup_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s))
    (hne : s.Nonempty) : l (⨆ i : s, f i) = ⨆ i : s, l (f i) := by
  haveI := hne.to_subtype
  rw [image_eq_range] at hf
  exact gc.l_ciSup hf

Galois Connection Preserves Indexed Supremum over Nonempty Bounded Sets

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois connection (i.e., for all $x \in \alpha$ and $y \in \beta$, $l(x) \leq y \leftrightarrow x \leq u(y)$). For any nonempty set $s \subseteq \gamma$ and any function $f : \gamma \to \alpha$ such that the image $f(s)$ is bounded above, the image under $l$ of the indexed supremum of $f$ over $s$ equals the indexed supremum of $l \circ f$ over $s$, i.e., $l(\bigsqcup_{i \in s} f(i)) = \bigsqcup_{i \in s} l(f(i))$.

GaloisConnection.u_csInf theorem

(gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) : u (sInf s) = ⨅ x : s, u x

Full source

theorem u_csInf (gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) :
    u (sInf s) = ⨅ x : s, u x :=
  gc.dual.l_csSup hne hbdd

Galois Connection Preserves Infimum for Nonempty Bounded Sets

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois connection (i.e., for all $x \in \alpha$ and $y \in \beta$, $l(x) \leq y \leftrightarrow x \leq u(y)$). For any nonempty subset $s \subseteq \beta$ that is bounded below, the image of the infimum of $s$ under $u$ equals the indexed infimum of $u$ over $s$, i.e., $u(\inf s) = \bigsqcap_{x \in s} u(x)$.

GaloisConnection.u_csInf' theorem

(gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) : u (sInf s) = sInf (u '' s)

Full source

theorem u_csInf' (gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) :
    u (sInf s) = sInf (u '' s) :=
  gc.dual.l_csSup' hne hbdd

Galois Connection Preserves Infimum via Image of Set

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois connection (i.e., for all $x \in \alpha$ and $y \in \beta$, $l(x) \leq y \leftrightarrow x \leq u(y)$). For any nonempty subset $s \subseteq \beta$ that is bounded below, the image of the infimum of $s$ under $u$ equals the infimum of the image of $s$ under $u$, i.e., $u(\inf s) = \inf (u \text{''} s)$.

GaloisConnection.u_ciInf theorem

(gc : GaloisConnection l u) {f : ι → β} (hf : BddBelow (range f)) : u (⨅ i, f i) = ⨅ i, u (f i)

Full source

theorem u_ciInf (gc : GaloisConnection l u) {f : ι → β} (hf : BddBelow (range f)) :
    u (⨅ i, f i) = ⨅ i, u (f i) :=
  gc.dual.l_ciSup hf

Galois Connection Preserves Indexed Infimum for Bounded Functions

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois connection (i.e., for all $x \in \alpha$ and $y \in \beta$, $l(x) \leq y \leftrightarrow x \leq u(y)$). For any function $f : \iota \to \beta$ whose range is bounded below, the image under $u$ of the indexed infimum of $f$ equals the indexed infimum of $u \circ f$, i.e., $u(\bigsqcap_{i} f(i)) = \bigsqcap_{i} u(f(i))$.

GaloisConnection.u_ciInf_set theorem

 (gc : GaloisConnection l u) {s : Set γ} {f : γ → β} (hf : BddBelow (f '' s)) (hne : s.Nonempty) :
  u (⨅ i : s, f i) = ⨅ i : s, u (f i)

Full source

theorem u_ciInf_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → β} (hf : BddBelow (f '' s))
    (hne : s.Nonempty) : u (⨅ i : s, f i) = ⨅ i : s, u (f i) :=
  gc.dual.l_ciSup_set hf hne

Galois Connection Preserves Indexed Infimum over Nonempty Bounded Sets

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $l : \alpha \to \beta$ and $u : \beta \to \alpha$ form a Galois connection (i.e., for all $x \in \alpha$ and $y \in \beta$, $l(x) \leq y \leftrightarrow x \leq u(y)$). For any nonempty set $s \subseteq \gamma$ and any function $f : \gamma \to \beta$ such that the image $f(s)$ is bounded below, the image under $u$ of the indexed infimum of $f$ over $s$ equals the indexed infimum of $u \circ f$ over $s$, i.e., $u(\bigsqcap_{i \in s} f(i)) = \bigsqcap_{i \in s} u(f(i))$.

OrderIso.map_csSup theorem

(e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : e (sSup s) = ⨆ x : s, e x

Full source

theorem map_csSup (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
    e (sSup s) = ⨆ x : s, e x :=
  e.to_galoisConnection.l_csSup hne hbdd

Order Isomorphism Preserves Supremum for Nonempty Bounded Sets

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $e : \alpha \to \beta$ be an order isomorphism. For any nonempty subset $s \subseteq \alpha$ that is bounded above, the image of the supremum of $s$ under $e$ equals the indexed supremum of $e$ over $s$, i.e., $e(\sup s) = \bigsqcup_{x \in s} e(x)$.

OrderIso.map_csSup' theorem

(e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : e (sSup s) = sSup (e '' s)

Full source

theorem map_csSup' (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
    e (sSup s) = sSup (e '' s) :=
  e.to_galoisConnection.l_csSup' hne hbdd

Order Isomorphism Preserves Supremum via Image of Set

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $e : \alpha \to \beta$ be an order isomorphism. For any nonempty subset $s \subseteq \alpha$ that is bounded above, the image of the supremum of $s$ under $e$ equals the supremum of the image of $s$ under $e$, i.e., $e(\sup s) = \sup (e \text{''} s)$.

OrderIso.map_ciSup theorem

(e : α ≃o β) {f : ι → α} (hf : BddAbove (range f)) : e (⨆ i, f i) = ⨆ i, e (f i)

Full source

theorem map_ciSup (e : α ≃o β) {f : ι → α} (hf : BddAbove (range f)) :
    e (⨆ i, f i) = ⨆ i, e (f i) :=
  e.to_galoisConnection.l_ciSup hf

Order Isomorphism Preserves Indexed Supremum for Bounded Functions

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $e : \alpha \to \beta$ be an order isomorphism. For any function $f : \iota \to \alpha$ whose range is bounded above, the image under $e$ of the indexed supremum of $f$ equals the indexed supremum of $e \circ f$, i.e., $e(\bigsqcup_{i} f(i)) = \bigsqcup_{i} e(f(i))$.

OrderIso.map_ciSup_set theorem

 (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s)) (hne : s.Nonempty) : e (⨆ i : s, f i) = ⨆ i : s, e (f i)

Full source

theorem map_ciSup_set (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s))
    (hne : s.Nonempty) : e (⨆ i : s, f i) = ⨆ i : s, e (f i) :=
  e.to_galoisConnection.l_ciSup_set hf hne

Order Isomorphism Preserves Indexed Supremum over Nonempty Bounded Sets

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $e : \alpha \to \beta$ be an order isomorphism. For any nonempty set $s \subseteq \gamma$ and any function $f : \gamma \to \alpha$ such that the image $f(s)$ is bounded above, the image under $e$ of the indexed supremum of $f$ over $s$ equals the indexed supremum of $e \circ f$ over $s$, i.e., $e(\bigsqcup_{i \in s} f(i)) = \bigsqcup_{i \in s} e(f(i))$.

OrderIso.map_csInf theorem

(e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) : e (sInf s) = ⨅ x : s, e x

Full source

theorem map_csInf (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) :
    e (sInf s) = ⨅ x : s, e x :=
  e.dual.map_csSup hne hbdd

Order Isomorphism Preserves Infimum for Nonempty Bounded Sets

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $e : \alpha \to \beta$ be an order isomorphism. For any nonempty subset $s \subseteq \alpha$ that is bounded below, the image of the infimum of $s$ under $e$ equals the indexed infimum of $e$ over $s$, i.e., $e(\inf s) = \bigsqcap_{x \in s} e(x)$.

OrderIso.map_csInf' theorem

(e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) : e (sInf s) = sInf (e '' s)

Full source

theorem map_csInf' (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) :
    e (sInf s) = sInf (e '' s) :=
  e.dual.map_csSup' hne hbdd

Order Isomorphism Preserves Infimum via Image of Set

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $e : \alpha \to \beta$ be an order isomorphism. For any nonempty subset $s \subseteq \alpha$ that is bounded below, the image of the infimum of $s$ under $e$ equals the infimum of the image of $s$ under $e$, i.e., $e(\inf s) = \inf (e \text{''} s)$.

OrderIso.map_ciInf theorem

(e : α ≃o β) {f : ι → α} (hf : BddBelow (range f)) : e (⨅ i, f i) = ⨅ i, e (f i)

Full source

theorem map_ciInf (e : α ≃o β) {f : ι → α} (hf : BddBelow (range f)) :
    e (⨅ i, f i) = ⨅ i, e (f i) :=
  e.dual.map_ciSup hf

Order Isomorphism Preserves Indexed Infimum for Bounded Functions

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $e : \alpha \to \beta$ be an order isomorphism. For any function $f : \iota \to \alpha$ whose range is bounded below, the image under $e$ of the indexed infimum of $f$ equals the indexed infimum of $e \circ f$, i.e., $e(\bigsqcap_{i} f(i)) = \bigsqcap_{i} e(f(i))$.

OrderIso.map_ciInf_set theorem

 (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddBelow (f '' s)) (hne : s.Nonempty) : e (⨅ i : s, f i) = ⨅ i : s, e (f i)

Full source

theorem map_ciInf_set (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddBelow (f '' s))
    (hne : s.Nonempty) : e (⨅ i : s, f i) = ⨅ i : s, e (f i) :=
  e.dual.map_ciSup_set hf hne

Order Isomorphism Preserves Indexed Infimum over Nonempty Bounded Sets

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $e : \alpha \to \beta$ be an order isomorphism. For any nonempty set $s \subseteq \gamma$ and any function $f : \gamma \to \alpha$ such that the image $f(s)$ is bounded below, the image under $e$ of the indexed infimum of $f$ over $s$ equals the indexed infimum of $e \circ f$ over $s$, i.e., $e(\bigsqcap_{i \in s} f(i)) = \bigsqcap_{i \in s} e(f(i))$.

OrderIso.map_ciSup' theorem

(e : α ≃o β) (f : ι → α) : e (⨆ i, f i) = ⨆ i, e (f i)

Full source

@[simp]
lemma map_ciSup' (e : α ≃o β) (f : ι → α) : e (⨆ i, f i) = ⨆ i, e (f i) := by
  cases isEmpty_or_nonempty ι
  · simp [map_bot]
  by_cases hf : BddAbove (range f)
  · exact e.map_ciSup hf
  · have hfe : ¬ BddAbove (range fun i ↦ e (f i)) := by
      simpa [Set.Nonempty, BddAbove, upperBounds, e.surjective.forall] using hf
    simp [map_bot, hf, hfe]

Order Isomorphism Preserves Indexed Supremum (Unbounded Case)

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $e : \alpha \to \beta$ be an order isomorphism. For any function $f : \iota \to \alpha$, the image under $e$ of the indexed supremum of $f$ equals the indexed supremum of $e \circ f$, i.e., $e(\bigsqcup_{i} f(i)) = \bigsqcup_{i} e(f(i))$.

WithTop.iSup_coe_eq_top theorem

: ⨆ x, (f x : WithTop α) = ⊤ ↔ ¬BddAbove (range f)

Full source

lemma iSup_coe_eq_top : ⨆ x, (f x : WithTop α)⨆ x, (f x : WithTop α) = ⊤ ↔ ¬BddAbove (range f) := by
  rw [iSup_eq_top, not_bddAbove_iff]
  refine ⟨fun hf r => ?_, fun hf a ha => ?_⟩
  · rcases hf r (WithTop.coe_lt_top r) with ⟨i, hi⟩
    exact ⟨f i, ⟨i, rfl⟩, WithTop.coe_lt_coe.mp hi⟩
  · rcases hf (a.untop ha.ne) with ⟨-, ⟨i, rfl⟩, hi⟩
    exact ⟨i, by simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi⟩

Supremum Equals Top in `WithTop α` if and only if Range is Unbounded Above

Informal description

For a function $f$ mapping into a type $\alpha$ with a top element $\top$ (denoted as `WithTop α`), the supremum of the range of $f$ equals $\top$ if and only if the range of $f$ is not bounded above.

WithTop.iSup_coe_lt_top theorem

: ⨆ x, (f x : WithTop α) < ⊤ ↔ BddAbove (range f)

Full source

lemma iSup_coe_lt_top : ⨆ x, (f x : WithTop α)⨆ x, (f x : WithTop α) < ⊤ ↔ BddAbove (range f) :=
  lt_top_iff_ne_top.trans iSup_coe_eq_top.not_left

Supremum in $\text{WithTop} \alpha$ is strictly less than top if and only if range is bounded above

Informal description

For a function $f$ mapping into a type $\alpha$ with a top element $\top$ (denoted as $\text{WithTop} \alpha$), the supremum of the range of $f$ is strictly less than $\top$ if and only if the range of $f$ is bounded above.

WithTop.iInf_coe_eq_top theorem

: ⨅ x, (f x : WithTop α) = ⊤ ↔ IsEmpty ι

Full source

lemma iInf_coe_eq_top : ⨅ x, (f x : WithTop α)⨅ x, (f x : WithTop α) = ⊤ ↔ IsEmpty ι := by simp [isEmpty_iff]

Infimum in $\text{WithTop} \alpha$ equals top if and only if index type is empty

Informal description

The infimum of a family of elements $(f x : \alpha)$ in $\text{WithTop} \alpha$ equals the top element $\top$ if and only if the index type $\iota$ is empty. In other words, $\bigsqcap_{x} (f x : \text{WithTop} \alpha) = \top \leftrightarrow \text{IsEmpty} \iota$.

WithTop.iInf_coe_lt_top theorem

: ⨅ i, (f i : WithTop α) < ⊤ ↔ Nonempty ι

Full source

lemma iInf_coe_lt_top : ⨅ i, (f i : WithTop α)⨅ i, (f i : WithTop α) < ⊤ ↔ Nonempty ι := by
  rw [lt_top_iff_ne_top, Ne, iInf_coe_eq_top, not_isEmpty_iff]

Infimum in $\text{WithTop} \alpha$ is less than top if and only if index type is nonempty

Informal description

The infimum of a family of elements $(f i : \alpha)$ in $\text{WithTop} \alpha$ is strictly less than the top element $\top$ if and only if the index type $\iota$ is nonempty. In other words, $\bigsqcap_{i} (f i : \text{WithTop} \alpha) < \top \leftrightarrow \text{Nonempty} \iota$.