Mathlib.Order.CompleteLattice.Lemmas

iSup_bool_eq theorem

{f : Bool → α} : ⨆ b : Bool, f b = f true ⊔ f false

Full source

theorem iSup_bool_eq {f : Bool → α} : ⨆ b : Bool, f b = f true ⊔ f false := by
  rw [iSup, Bool.range_eq, sSup_pair, sup_comm]

Supremum over Booleans Equals Join of Values: $\bigsqcup_{b \in \text{Bool}} f(b) = f(\text{true}) \sqcup f(\text{false})$

Informal description

For any function $f$ from the boolean type to a complete lattice $\alpha$, the supremum of $f$ over all boolean values is equal to the join of $f(\text{true})$ and $f(\text{false})$, i.e., \[ \bigsqcup_{b \in \text{Bool}} f(b) = f(\text{true}) \sqcup f(\text{false}). \]

iInf_bool_eq theorem

{f : Bool → α} : ⨅ b : Bool, f b = f true ⊓ f false

Full source

theorem iInf_bool_eq {f : Bool → α} : ⨅ b : Bool, f b = f true ⊓ f false :=
  @iSup_bool_eq αᵒᵈ _ _

Infimum over Booleans Equals Meet of Values: $\bigsqcap_{b \in \text{Bool}} f(b) = f(\text{true}) \sqcap f(\text{false})$

Informal description

For any function $f$ from the boolean type to a complete lattice $\alpha$, the infimum of $f$ over all boolean values is equal to the meet of $f(\text{true})$ and $f(\text{false})$, i.e., \[ \bigsqcap_{b \in \text{Bool}} f(b) = f(\text{true}) \sqcap f(\text{false}). \]

sup_eq_iSup theorem

(x y : α) : x ⊔ y = ⨆ b : Bool, cond b x y

Full source

theorem sup_eq_iSup (x y : α) : x ⊔ y = ⨆ b : Bool, cond b x y := by
  rw [iSup_bool_eq, Bool.cond_true, Bool.cond_false]

Supremum as Boolean-indexed Supremum: $x \sqcup y = \bigsqcup_{b \in \text{Bool}} \text{cond}(b, x, y)$

Informal description

For any two elements $x$ and $y$ in a complete lattice $\alpha$, their supremum $x \sqcup y$ is equal to the indexed supremum over the boolean type of the conditional expression $\text{cond}(b, x, y)$, i.e., \[ x \sqcup y = \bigsqcup_{b \in \text{Bool}} \text{cond}(b, x, y). \]

inf_eq_iInf theorem

(x y : α) : x ⊓ y = ⨅ b : Bool, cond b x y

Full source

theorem inf_eq_iInf (x y : α) : x ⊓ y = ⨅ b : Bool, cond b x y :=
  @sup_eq_iSup αᵒᵈ _ _ _

Infimum as Boolean-indexed Infimum: $x \sqcap y = \bigsqcap_{b \in \text{Bool}} \text{cond}(b, x, y)$

Informal description

For any two elements $x$ and $y$ in a complete lattice $\alpha$, their infimum $x \sqcap y$ is equal to the indexed infimum over the boolean type of the conditional expression $\text{cond}(b, x, y)$, i.e., \[ x \sqcap y = \bigsqcap_{b \in \text{Bool}} \text{cond}(b, x, y). \]

iSup_ge_eq_iSup_nat_add theorem

(u : ℕ → α) (n : ℕ) : ⨆ i ≥ n, u i = ⨆ i, u (i + n)

Full source

theorem iSup_ge_eq_iSup_nat_add (u : ℕ → α) (n : ℕ) : ⨆ i ≥ n, u i = ⨆ i, u (i + n) := by
  apply le_antisymm <;> simp only [iSup_le_iff]
  · refine fun i hi => le_sSup ⟨i - n, ?_⟩
    dsimp only
    rw [Nat.sub_add_cancel hi]
  · exact fun i => le_sSup ⟨i + n, iSup_pos (Nat.le_add_left _ _)⟩

Supremum of Tail Equals Supremum of Shifted Sequence

Informal description

For any sequence $u : \mathbb{N} \to \alpha$ in a complete lattice $\alpha$ and any natural number $n$, the supremum of the tail of the sequence starting from index $n$ is equal to the supremum of the sequence shifted by $n$. That is, \[ \bigsqcup_{i \geq n} u_i = \bigsqcup_{i} u_{i+n}. \]

iInf_ge_eq_iInf_nat_add theorem

(u : ℕ → α) (n : ℕ) : ⨅ i ≥ n, u i = ⨅ i, u (i + n)

Full source

theorem iInf_ge_eq_iInf_nat_add (u : ℕ → α) (n : ℕ) : ⨅ i ≥ n, u i = ⨅ i, u (i + n) :=
  @iSup_ge_eq_iSup_nat_add αᵒᵈ _ _ _

Infimum of Tail Equals Infimum of Shifted Sequence

Informal description

For any sequence $u : \mathbb{N} \to \alpha$ in a complete lattice $\alpha$ and any natural number $n$, the infimum of the tail of the sequence starting from index $n$ is equal to the infimum of the sequence shifted by $n$. That is, \[ \bigsqcap_{i \geq n} u_i = \bigsqcap_{i} u_{i+n}. \]

Monotone.iSup_nat_add theorem

{f : ℕ → α} (hf : Monotone f) (k : ℕ) : ⨆ n, f (n + k) = ⨆ n, f n

Full source

theorem Monotone.iSup_nat_add {f : ℕ → α} (hf : Monotone f) (k : ℕ) : ⨆ n, f (n + k) = ⨆ n, f n :=
  le_antisymm (iSup_le fun i => le_iSup _ (i + k)) <| iSup_mono fun i => hf <| Nat.le_add_right i k

Supremum of Shifted Monotone Sequence Equals Original Supremum

Informal description

For any monotone sequence $f : \mathbb{N} \to \alpha$ in a complete lattice $\alpha$ and any natural number $k$, the supremum of the shifted sequence $(f(n + k))_{n \in \mathbb{N}}$ is equal to the supremum of the original sequence $(f(n))_{n \in \mathbb{N}}$. That is, \[ \bigsqcup_{n} f(n + k) = \bigsqcup_{n} f(n). \]

Antitone.iInf_nat_add theorem

{f : ℕ → α} (hf : Antitone f) (k : ℕ) : ⨅ n, f (n + k) = ⨅ n, f n

Full source

theorem Antitone.iInf_nat_add {f : ℕ → α} (hf : Antitone f) (k : ℕ) : ⨅ n, f (n + k) = ⨅ n, f n :=
  hf.dual_right.iSup_nat_add k

Infimum of Shifted Antitone Sequence Equals Original Infimum

Informal description

For any antitone sequence $f : \mathbb{N} \to \alpha$ in a complete lattice $\alpha$ and any natural number $k$, the infimum of the shifted sequence $(f(n + k))_{n \in \mathbb{N}}$ is equal to the infimum of the original sequence $(f(n))_{n \in \mathbb{N}}$. That is, \[ \bigsqcap_{n} f(n + k) = \bigsqcap_{n} f(n). \]

iSup_iInf_ge_nat_add theorem

(f : ℕ → α) (k : ℕ) : ⨆ n, ⨅ i ≥ n, f (i + k) = ⨆ n, ⨅ i ≥ n, f i

Full source

theorem iSup_iInf_ge_nat_add (f : ℕ → α) (k : ℕ) :
    ⨆ n, ⨅ i ≥ n, f (i + k) = ⨆ n, ⨅ i ≥ n, f i := by
  have hf : Monotone fun n => ⨅ i ≥ n, f i := fun n m h => biInf_mono fun i => h.trans
  rw [← Monotone.iSup_nat_add hf k]
  · simp_rw [iInf_ge_eq_iInf_nat_add, ← Nat.add_assoc]

Supremum of Infima of Shifted Sequence Equals Supremum of Infima of Original Sequence

Informal description

For any sequence $f : \mathbb{N} \to \alpha$ in a complete lattice $\alpha$ and any natural number $k$, the supremum over $n$ of the infima of $f$ over indices $i \geq n$ shifted by $k$ is equal to the supremum over $n$ of the infima of $f$ over indices $i \geq n$. In symbols: \[ \bigsqcup_{n} \bigsqcap_{i \geq n} f(i + k) = \bigsqcup_{n} \bigsqcap_{i \geq n} f(i). \]

iInf_iSup_ge_nat_add theorem

: ∀ (f : ℕ → α) (k : ℕ), ⨅ n, ⨆ i ≥ n, f (i + k) = ⨅ n, ⨆ i ≥ n, f i

Full source

theorem iInf_iSup_ge_nat_add :
    ∀ (f : ℕ → α) (k : ℕ), ⨅ n, ⨆ i ≥ n, f (i + k) = ⨅ n, ⨆ i ≥ n, f i :=
  @iSup_iInf_ge_nat_add αᵒᵈ _

Infimum of Suprema of Shifted Sequence Equals Infimum of Suprema of Original Sequence

Informal description

For any sequence $f \colon \mathbb{N} \to \alpha$ in a complete lattice $\alpha$ and any natural number $k$, the infimum over $n$ of the suprema of $f$ over indices $i \geq n$ shifted by $k$ is equal to the infimum over $n$ of the suprema of $f$ over indices $i \geq n$. In symbols: \[ \bigsqcap_{n} \bigsqcup_{i \geq n} f(i + k) = \bigsqcap_{n} \bigsqcup_{i \geq n} f(i). \]

sup_iSup_nat_succ theorem

(u : ℕ → α) : (u 0 ⊔ ⨆ i, u (i + 1)) = ⨆ i, u i

Full source

theorem sup_iSup_nat_succ (u : ℕ → α) : (u 0 ⊔ ⨆ i, u (i + 1)) = ⨆ i, u i :=
  calc
    (u 0 ⊔ ⨆ i, u (i + 1)) = ⨆ x ∈ {0} ∪ range Nat.succ, u x := by
      { rw [iSup_union, iSup_singleton, iSup_range] }
    _ = ⨆ i, u i := by rw [Nat.zero_union_range_succ, iSup_univ]

Join of First Term and Supremum of Shifted Sequence Equals Supremum of Original Sequence

Informal description

For any sequence $u : \mathbb{N} \to \alpha$ in a complete lattice $\alpha$, the join of the first term $u(0)$ and the supremum of the shifted sequence $(u(i+1))_{i \in \mathbb{N}}$ equals the supremum of the entire sequence $(u(i))_{i \in \mathbb{N}}$. In symbols: \[ u(0) \sqcup \left(\bigsqcup_{i} u(i+1)\right) = \bigsqcup_{i} u(i). \]

inf_iInf_nat_succ theorem

(u : ℕ → α) : (u 0 ⊓ ⨅ i, u (i + 1)) = ⨅ i, u i

Full source

theorem inf_iInf_nat_succ (u : ℕ → α) : (u 0 ⊓ ⨅ i, u (i + 1)) = ⨅ i, u i :=
  @sup_iSup_nat_succ αᵒᵈ _ u

Meet of First Term and Infimum of Shifted Sequence Equals Infimum of Original Sequence

Informal description

For any sequence $u \colon \mathbb{N} \to \alpha$ in a complete lattice $\alpha$, the meet of the first term $u(0)$ and the infimum of the shifted sequence $(u(i+1))_{i \in \mathbb{N}}$ equals the infimum of the entire sequence $(u(i))_{i \in \mathbb{N}}$. In symbols: \[ u(0) \sqcap \left(\bigsqcap_{i} u(i+1)\right) = \bigsqcap_{i} u(i). \]

iInf_nat_gt_zero_eq theorem

(f : ℕ → α) : ⨅ i > 0, f i = ⨅ i, f (i + 1)

Full source

theorem iInf_nat_gt_zero_eq (f : ℕ → α) : ⨅ i > 0, f i = ⨅ i, f (i + 1) := by
  rw [← iInf_range, Nat.range_succ]
  simp

Infimum of Positive Terms Equals Infimum of Shifted Sequence: $\bigsqcap_{i>0} f(i) = \bigsqcap_i f(i+1)$

Informal description

For any sequence $f : \mathbb{N} \to \alpha$ in a complete lattice $\alpha$, the infimum of the terms $f(i)$ over all positive natural numbers $i > 0$ is equal to the infimum of the shifted sequence $f(i+1)$ over all natural numbers $i$. In symbols: \[ \bigsqcap_{i > 0} f(i) = \bigsqcap_{i} f(i+1). \]

iSup_nat_gt_zero_eq theorem

(f : ℕ → α) : ⨆ i > 0, f i = ⨆ i, f (i + 1)

Full source

theorem iSup_nat_gt_zero_eq (f : ℕ → α) : ⨆ i > 0, f i = ⨆ i, f (i + 1) :=
  @iInf_nat_gt_zero_eq αᵒᵈ _ f

Supremum of Positive Terms Equals Supremum of Shifted Sequence: $\bigsqcup_{i>0} f(i) = \bigsqcup_i f(i+1)$

Informal description

For any sequence $f \colon \mathbb{N} \to \alpha$ in a complete lattice $\alpha$, the supremum of the terms $f(i)$ over all positive natural numbers $i > 0$ is equal to the supremum of the shifted sequence $f(i+1)$ over all natural numbers $i$. In symbols: \[ \bigsqcup_{i > 0} f(i) = \bigsqcup_{i} f(i+1). \]

sup_sInf_le_iInf_sup theorem

: a ⊔ sInf s ≤ ⨅ b ∈ s, a ⊔ b

Full source

/-- This is a weaker version of `sup_sInf_eq` -/
theorem sup_sInf_le_iInf_sup : a ⊔ sInf s ≤ ⨅ b ∈ s, a ⊔ b :=
  le_iInf₂ fun _ h => sup_le_sup_left (sInf_le h) _

Supremum-Infimum Inequality: $a \sqcup \bigwedge s \leq \bigsqcap_{b \in s} (a \sqcup b)$

Informal description

For any element $a$ in a complete lattice $\alpha$ and any subset $s \subseteq \alpha$, the supremum of $a$ with the infimum of $s$ is less than or equal to the infimum over all $b \in s$ of the supremum of $a$ with $b$, i.e., \[ a \sqcup \bigwedge s \leq \bigsqcap_{b \in s} (a \sqcup b). \]

iSup_inf_le_inf_sSup theorem

: ⨆ b ∈ s, a ⊓ b ≤ a ⊓ sSup s

Full source

/-- This is a weaker version of `inf_sSup_eq` -/
theorem iSup_inf_le_inf_sSup : ⨆ b ∈ s, a ⊓ b ≤ a ⊓ sSup s :=
  @sup_sInf_le_iInf_sup αᵒᵈ _ _ _

Supremum-Infimum Inequality: $\bigsqcup_{b \in s} (a \sqcap b) \leq a \sqcap \bigsqcup s$

Informal description

For any element $a$ in a complete lattice $\alpha$ and any subset $s \subseteq \alpha$, the supremum over all $b \in s$ of the infimum of $a$ with $b$ is less than or equal to the infimum of $a$ with the supremum of $s$, i.e., \[ \bigsqcup_{b \in s} (a \sqcap b) \leq a \sqcap \bigsqcup s. \]

sInf_sup_le_iInf_sup theorem

: sInf s ⊔ a ≤ ⨅ b ∈ s, b ⊔ a

Full source

/-- This is a weaker version of `sInf_sup_eq` -/
theorem sInf_sup_le_iInf_sup : sInfsInf s ⊔ a ≤ ⨅ b ∈ s, b ⊔ a :=
  le_iInf₂ fun _ h => sup_le_sup_right (sInf_le h) _

Infimum-Supremum Inequality in Complete Lattices: $(\bigwedge s) \sqcup a \leq \bigwedge_{b \in s} (b \sqcup a)$

Informal description

In a complete lattice $\alpha$, for any subset $s \subseteq \alpha$ and any element $a \in \alpha$, the supremum of the infimum of $s$ with $a$ is less than or equal to the infimum of the suprema of each element $b \in s$ with $a$. That is, \[ \left(\bigwedge s\right) \sqcup a \leq \bigwedge_{b \in s} (b \sqcup a). \]

iSup_inf_le_sSup_inf theorem

: ⨆ b ∈ s, b ⊓ a ≤ sSup s ⊓ a

Full source

/-- This is a weaker version of `sSup_inf_eq` -/
theorem iSup_inf_le_sSup_inf : ⨆ b ∈ s, b ⊓ a ≤ sSupsSup s ⊓ a :=
  @sInf_sup_le_iInf_sup αᵒᵈ _ _ _

Supremum-Infimum Inequality in Complete Lattices: $\bigsqcup_{b \in s} (b \sqcap a) \leq (\bigsqcup s) \sqcap a$

Informal description

In a complete lattice $\alpha$, for any subset $s \subseteq \alpha$ and any element $a \in \alpha$, the supremum of the infima of each element $b \in s$ with $a$ is less than or equal to the infimum of the supremum of $s$ with $a$. That is, \[ \bigsqcup_{b \in s} (b \sqcap a) \leq \left(\bigsqcup s\right) \sqcap a. \]

le_iSup_inf_iSup theorem

(f g : ι → α) : ⨆ i, f i ⊓ g i ≤ (⨆ i, f i) ⊓ ⨆ i, g i

Full source

theorem le_iSup_inf_iSup (f g : ι → α) : ⨆ i, f i ⊓ g i ≤ (⨆ i, f i) ⊓ ⨆ i, g i :=
  le_inf (iSup_mono fun _ => inf_le_left) (iSup_mono fun _ => inf_le_right)

Supremum-Infimum Inequality: $\bigsqcup_i (f_i \sqcap g_i) \leq (\bigsqcup_i f_i) \sqcap (\bigsqcup_i g_i)$

Informal description

For any indexed families of elements $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ in a complete lattice $\alpha$, the supremum of the pairwise infima $f_i \sqcap g_i$ is less than or equal to the infimum of the suprema of $f_i$ and $g_i$ separately. That is, \[ \bigsqcup_i (f_i \sqcap g_i) \leq \left(\bigsqcup_i f_i\right) \sqcap \left(\bigsqcup_i g_i\right). \]

iInf_sup_iInf_le theorem

(f g : ι → α) : (⨅ i, f i) ⊔ ⨅ i, g i ≤ ⨅ i, f i ⊔ g i

Full source

theorem iInf_sup_iInf_le (f g : ι → α) : (⨅ i, f i) ⊔ ⨅ i, g i ≤ ⨅ i, f i ⊔ g i :=
  @le_iSup_inf_iSup αᵒᵈ ι _ f g

Infimum-Supremum Inequality: $(\bigsqcap_i f_i) \sqcup (\bigsqcap_i g_i) \leq \bigsqcap_i (f_i \sqcup g_i)$

Informal description

For any indexed families of elements $(f_i)_{i \in \iota}$ and $(g_i)_{i \in \iota}$ in a complete lattice $\alpha$, the supremum of the infima of $f_i$ and $g_i$ is less than or equal to the infimum of the pairwise suprema $f_i \sqcup g_i$. That is, \[ \left(\bigsqcap_i f_i\right) \sqcup \left(\bigsqcap_i g_i\right) \leq \bigsqcap_i (f_i \sqcup g_i). \]

disjoint_sSup_left theorem

{a : Set α} {b : α} (d : Disjoint (sSup a) b) {i} (hi : i ∈ a) : Disjoint i b

Full source

theorem disjoint_sSup_left {a : Set α} {b : α} (d : Disjoint (sSup a) b) {i} (hi : i ∈ a) :
    Disjoint i b :=
  disjoint_iff_inf_le.mpr (iSup₂_le_iff.1 (iSup_inf_le_sSup_inf.trans d.le_bot) i hi :)

Disjointness Propagation from Supremum to Elements: $\bigsqcup a \perp b \Rightarrow \forall i \in a, i \perp b$

Informal description

Let $\alpha$ be a complete lattice, $a$ a subset of $\alpha$, and $b$ an element of $\alpha$. If the supremum of $a$ is disjoint with $b$ (i.e., $\bigsqcup a \sqcap b = \bot$), then every element $i \in a$ is also disjoint with $b$ (i.e., $i \sqcap b = \bot$).

disjoint_sSup_right theorem

{a : Set α} {b : α} (d : Disjoint b (sSup a)) {i} (hi : i ∈ a) : Disjoint b i

Full source

theorem disjoint_sSup_right {a : Set α} {b : α} (d : Disjoint b (sSup a)) {i} (hi : i ∈ a) :
    Disjoint b i :=
  disjoint_iff_inf_le.mpr (iSup₂_le_iff.mp (iSup_inf_le_inf_sSup.trans d.le_bot) i hi :)

Disjointness Propagation from Supremum to Elements: $b \sqcap \bigvee a = \bot \implies \forall i \in a, b \sqcap i = \bot$

Informal description

Let $\alpha$ be a complete lattice, $a \subseteq \alpha$ a subset, and $b \in \alpha$ an element. If $b$ is disjoint from the supremum of $a$ (i.e., $b \sqcap \bigvee a = \bot$), then for every element $i \in a$, $b$ is disjoint from $i$ (i.e., $b \sqcap i = \bot$).

disjoint_of_sSup_disjoint_of_le_of_le theorem

 {a b : α} {c d : Set α} (hs : ∀ e ∈ c, e ≤ a) (ht : ∀ e ∈ d, e ≤ b) (hd : Disjoint a b) (he : ⊥ ∉ c ∨ ⊥ ∉ d) :
  Disjoint c d

Full source

lemma disjoint_of_sSup_disjoint_of_le_of_le {a b : α} {c d : Set α} (hs : ∀ e ∈ c, e ≤ a)
    (ht : ∀ e ∈ d, e ≤ b) (hd : Disjoint a b) (he : ⊥⊥ ∉ c⊥ ∉ c ∨ ⊥ ∉ d) : Disjoint c d := by
  rw [disjoint_iff_forall_ne]
  intros x hx y hy
  rw [Disjoint.ne_iff]
  · aesop
  · exact Disjoint.mono (hs x hx) (ht y hy) hd

Disjointness of Sets under Supremum Conditions in Complete Lattices

Informal description

Let $\alpha$ be a complete lattice with elements $a, b$ and sets $c, d \subseteq \alpha$. Suppose that: 1. Every element $e \in c$ satisfies $e \leq a$, 2. Every element $e \in d$ satisfies $e \leq b$, 3. $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), and 4. Either $\bot \notin c$ or $\bot \notin d$. Then the sets $c$ and $d$ are disjoint (i.e., $c \cap d = \emptyset$).

disjoint_of_sSup_disjoint theorem

{a b : Set α} (hd : Disjoint (sSup a) (sSup b)) (he : ⊥ ∉ a ∨ ⊥ ∉ b) : Disjoint a b

Full source

lemma disjoint_of_sSup_disjoint {a b : Set α} (hd : Disjoint (sSup a) (sSup b))
    (he : ⊥⊥ ∉ a⊥ ∉ a ∨ ⊥ ∉ b) : Disjoint a b :=
  disjoint_of_sSup_disjoint_of_le_of_le (fun _ hc ↦ le_sSup hc) (fun _ hc ↦ le_sSup hc) hd he

Disjointness of Sets via Suprema in Complete Lattices

Informal description

Let $\alpha$ be a complete lattice, and let $a, b \subseteq \alpha$ be two subsets. If the suprema of $a$ and $b$ are disjoint (i.e., $\bigvee a \sqcap \bigvee b = \bot$) and either $\bot \notin a$ or $\bot \notin b$, then $a$ and $b$ are disjoint (i.e., $a \cap b = \emptyset$).

ULift.supSet instance

[SupSet α] : SupSet (ULift.{v} α)

Full source

instance supSet [SupSet α] : SupSet (ULift.{v} α) where sSup s := ULift.up (sSup <| ULift.upULift.up ⁻¹' s)

Supremum Operator on Lifted Types

Informal description

For any type $\alpha$ equipped with a supremum operator $\operatorname{sSup}$, the lifted type $\operatorname{ULift} \alpha$ also has a supremum operator, where the supremum of a set $s$ in $\operatorname{ULift} \alpha$ is obtained by lifting the supremum of the preimage of $s$ under the down projection.

ULift.down_sSup theorem

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

Full source

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

Supremum Commutes with Down Projection in Lifted Types

Informal description

For any type $\alpha$ with a supremum operator $\operatorname{sSup}$ and any set $s$ in the lifted type $\operatorname{ULift} \alpha$, the down projection of the supremum of $s$ equals the supremum of the preimage of $s$ under the up projection. That is, $(\operatorname{sSup} s).\text{down} = \operatorname{sSup} (\text{ULift.up}^{-1}(s))$.

ULift.up_sSup theorem

[SupSet α] (s : Set α) : up (sSup s) = sSup (ULift.down ⁻¹' s)

Full source

theorem up_sSup [SupSet α] (s : Set α) : up (sSup s) = sSup (ULift.downULift.down ⁻¹' s) := rfl

Lifting Preserves Supremum: $\operatorname{up}(\operatorname{sSup} s) = \operatorname{sSup}(\operatorname{down}^{-1}(s))$

Informal description

For any type $\alpha$ with a supremum operator $\operatorname{sSup}$ and any subset $s \subseteq \alpha$, the lift of the supremum of $s$ is equal to the supremum of the preimage of $s$ under the down projection in the lifted type $\operatorname{ULift} \alpha$. That is, $\operatorname{up}(\operatorname{sSup} s) = \operatorname{sSup}(\operatorname{ULift.down}^{-1}(s))$.

ULift.infSet instance

[InfSet α] : InfSet (ULift.{v} α)

Full source

instance infSet [InfSet α] : InfSet (ULift.{v} α) where sInf s := ULift.up (sInf <| ULift.upULift.up ⁻¹' s)

Infimum Structure on Lifted Types

Informal description

For any type $\alpha$ equipped with an infimum structure, the lifted type $\text{ULift}\, \alpha$ also has an infimum structure, where the infimum of a set in $\text{ULift}\, \alpha$ is computed by lifting the infimum of the corresponding set in $\alpha$.

ULift.down_sInf theorem

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

Full source

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

Projection of Infimum in Lifted Type Equals Infimum of Preimage

Informal description

For any type $\alpha$ equipped with an infimum structure and any set $s$ of elements in the lifted type $\text{ULift}\, \alpha$, the infimum of $s$ in $\text{ULift}\, \alpha$ when projected back to $\alpha$ equals the infimum of the preimage of $s$ under the lifting operation in $\alpha$. That is, $(\bigwedge s).\text{down} = \bigwedge \{x \in \alpha \mid \text{up}(x) \in s\}$.

ULift.up_sInf theorem

[InfSet α] (s : Set α) : up (sInf s) = sInf (ULift.down ⁻¹' s)

Full source

theorem up_sInf [InfSet α] (s : Set α) : up (sInf s) = sInf (ULift.downULift.down ⁻¹' s) := rfl

Lifting Infimum to ULift via Preimage

Informal description

For any type $\alpha$ with an infimum structure and any subset $s \subseteq \alpha$, the lift of the infimum of $s$ in $\alpha$ is equal to the infimum of the preimage of $s$ under the down projection in the lifted type $\text{ULift}\, \alpha$. That is, $\text{up}(\inf s) = \inf (\text{down}^{-1}(s))$.

ULift.down_iSup theorem

[SupSet α] (f : ι → ULift.{v} α) : (⨆ i, f i).down = ⨆ i, (f i).down

Full source

theorem down_iSup [SupSet α] (f : ι → ULift.{v} α) : (⨆ i, f i).down = ⨆ i, (f i).down :=
  congr_arg sSup <| (preimage_eq_iff_eq_image ULift.up_bijective).mpr <|
    Eq.symm (range_comp _ _).symm

Projection of Indexed Supremum in Lifted Type Equals Supremum of Projections

Informal description

For any type $\alpha$ equipped with a supremum structure and any indexed family of elements $f : \iota \to \mathrm{ULift}\, \alpha$ in the lifted type, the projection of the supremum $\bigsqcup_i f_i$ back to $\alpha$ equals the supremum of the projections of the family elements. That is, $(\bigsqcup_i f_i).\mathrm{down} = \bigsqcup_i (f_i.\mathrm{down})$.

ULift.up_iSup theorem

[SupSet α] (f : ι → α) : up (⨆ i, f i) = ⨆ i, up (f i)

Full source

theorem up_iSup [SupSet α] (f : ι → α) : up (⨆ i, f i) = ⨆ i, up (f i) :=
  congr_arg ULift.up <| (down_iSup _).symm

Lifting Commutes with Indexed Supremum: $\mathrm{up}(\bigsqcup_i f(i)) = \bigsqcup_i \mathrm{up}(f(i))$

Informal description

For any type $\alpha$ equipped with a supremum structure and any indexed family of elements $f : \iota \to \alpha$, the lift of the supremum $\bigsqcup_i f(i)$ in $\alpha$ equals the supremum of the lifted elements $\bigsqcup_i \mathrm{up}(f(i))$ in the lifted type $\mathrm{ULift}\, \alpha$. That is, $\mathrm{up}(\bigsqcup_i f(i)) = \bigsqcup_i \mathrm{up}(f(i))$.

ULift.down_iInf theorem

[InfSet α] (f : ι → ULift.{v} α) : (⨅ i, f i).down = ⨅ i, (f i).down

Full source

theorem down_iInf [InfSet α] (f : ι → ULift.{v} α) : (⨅ i, f i).down = ⨅ i, (f i).down :=
  congr_arg sInf <| (preimage_eq_iff_eq_image ULift.up_bijective).mpr <|
    Eq.symm (range_comp _ _).symm

Infimum Commutes with Down Projection in Lifted Types: $(\bigsqcap_i f(i)).\mathrm{down} = \bigsqcap_i (f(i)).\mathrm{down}$

Informal description

For any type $\alpha$ equipped with an infimum structure and any indexed family of lifted elements $f : \iota \to \mathrm{ULift}\, \alpha$, the down projection of the infimum $\bigsqcap_i f(i)$ equals the infimum of the down projections $\bigsqcap_i (f(i)).\mathrm{down}$.

ULift.up_iInf theorem

[InfSet α] (f : ι → α) : up (⨅ i, f i) = ⨅ i, up (f i)

Full source

theorem up_iInf [InfSet α] (f : ι → α) : up (⨅ i, f i) = ⨅ i, up (f i) :=
  congr_arg ULift.up <| (down_iInf _).symm

Lifting Commutes with Infimum: $\mathrm{up}(\bigsqcap_i f(i)) = \bigsqcap_i \mathrm{up}(f(i))$

Informal description

For any type $\alpha$ equipped with an infimum structure and any indexed family $f : \iota \to \alpha$, the lifting of the infimum $\bigsqcap_i f(i)$ equals the infimum of the lifted elements $\bigsqcap_i \mathrm{up}(f(i))$.

ULift.instCompleteLattice instance

[CompleteLattice α] : CompleteLattice (ULift.{v} α)

Full source

instance instCompleteLattice [CompleteLattice α] : CompleteLattice (ULift.{v} α) :=
  ULift.down_injective.completeLattice _ down_sup down_inf
    (fun s => by rw [sSup_eq_iSup', down_iSup, iSup_subtype''])
    (fun s => by rw [sInf_eq_iInf', down_iInf, iInf_subtype'']) down_top down_bot

Complete Lattice Structure on Lifted Types

Informal description

For any complete lattice $\alpha$, the lifted type $\mathrm{ULift}\, \alpha$ is also a complete lattice, where all lattice operations are defined by lifting the corresponding operations from $\alpha$.

PUnit.instCompleteLinearOrder instance

: CompleteLinearOrder PUnit

Full source

instance instCompleteLinearOrder : CompleteLinearOrder PUnit where
  __ := instBooleanAlgebra
  __ := instLinearOrder
  sSup := fun _ => unit
  sInf := fun _ => unit
  le_sSup := by intros; trivial
  sSup_le := by intros; trivial
  sInf_le := by intros; trivial
  le_sInf := by intros; trivial
  le_himp_iff := by intros; trivial
  himp_bot := by intros; trivial
  sdiff_le_iff := by intros; trivial
  top_sdiff := by intros; trivial

Complete Linear Order on the Unit Type

Informal description

The trivial type `PUnit` (the type with a single element) is a complete linear order, where every subset has both a supremum and an infimum, and the order is total.

Mathlib.Order.CompleteLattice.Lemmas

Naming conventions

Notation