Mathlib.Data.Finset.Lattice.Union

Finset.sup_biUnion theorem

[DecidableEq β] (s : Finset γ) (t : γ → Finset β) : (s.biUnion t).sup f = s.sup fun x => (t x).sup f

Full source

@[simp]
theorem sup_biUnion [DecidableEq β] (s : Finset γ) (t : γ → Finset β) :
    (s.biUnion t).sup f = s.sup fun x => (t x).sup f :=
  eq_of_forall_ge_iff fun c => by simp [@forall_swap _ β]

Supremum over Union of Finite Sets Equals Iterated Supremum

Informal description

Let $\beta$ and $\gamma$ be types with decidable equality. Given a finite set $s \subseteq \gamma$ and a function $t : \gamma \to \mathcal{F}(\beta)$ (where $\mathcal{F}(\beta)$ denotes the type of finite subsets of $\beta$), the supremum of $f$ over the union $\bigcup_{x \in s} t(x)$ is equal to the supremum over $s$ of the function $x \mapsto \sup_{y \in t(x)} f(y)$. In symbols: \[ \sup \left( \bigcup_{x \in s} t(x) \right) f = \sup_{x \in s} \left( \sup_{y \in t(x)} f(y) \right) \]

Finset.inf_biUnion theorem

[DecidableEq β] (s : Finset γ) (t : γ → Finset β) : (s.biUnion t).inf f = s.inf fun x => (t x).inf f

Full source

@[simp] theorem inf_biUnion [DecidableEq β] (s : Finset γ) (t : γ → Finset β) :
    (s.biUnion t).inf f = s.inf fun x => (t x).inf f :=
  @sup_biUnion αᵒᵈ _ _ _ _ _ _ _ _

Infimum over Union of Finite Sets Equals Iterated Infimum

Informal description

Let $\beta$ and $\gamma$ be types with decidable equality. Given a finite set $s \subseteq \gamma$ and a function $t : \gamma \to \mathcal{F}(\beta)$ (where $\mathcal{F}(\beta)$ denotes the type of finite subsets of $\beta$), the infimum of $f$ over the union $\bigcup_{x \in s} t(x)$ is equal to the infimum over $s$ of the function $x \mapsto \inf_{y \in t(x)} f(y)$. In symbols: \[ \inf \left( \bigcup_{x \in s} t(x) \right) f = \inf_{x \in s} \left( \inf_{y \in t(x)} f(y) \right) \]

Finset.sup'_biUnion theorem

 [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β} (Ht : ∀ b, (t b).Nonempty) :
  (s.biUnion t).sup' (Hs.biUnion fun b _ => Ht b) f = s.sup' Hs (fun b => (t b).sup' (Ht b) f)

Full source

theorem sup'_biUnion [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β}
    (Ht : ∀ b, (t b).Nonempty) :
    (s.biUnion t).sup' (Hs.biUnion fun b _ => Ht b) f = s.sup' Hs (fun b => (t b).sup' (Ht b) f) :=
  eq_of_forall_ge_iff fun c => by simp [@forall_swap _ β]

Nonempty Supremum over Union Equals Iterated Nonempty Supremum

Informal description

Let $\beta$ and $\gamma$ be types with decidable equality. Given a nonempty finite set $s \subseteq \gamma$ and a function $t : \gamma \to \mathcal{F}(\beta)$ (where $\mathcal{F}(\beta)$ denotes the type of finite subsets of $\beta$) such that $t(b)$ is nonempty for every $b \in \gamma$, the supremum of $f$ over the union $\bigcup_{x \in s} t(x)$ is equal to the supremum over $s$ of the function $x \mapsto \sup'_{y \in t(x)} f(y)$. In symbols: \[ \sup' \left( \bigcup_{x \in s} t(x) \right) f = \sup'_{x \in s} \left( \sup'_{y \in t(x)} f(y) \right) \] where $\sup'$ denotes the supremum operation restricted to nonempty sets.

Finset.inf'_biUnion theorem

 [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β} (Ht : ∀ b, (t b).Nonempty) :
  (s.biUnion t).inf' (Hs.biUnion fun b _ => Ht b) f = s.inf' Hs (fun b => (t b).inf' (Ht b) f)

Full source

theorem inf'_biUnion [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β}
    (Ht : ∀ b, (t b).Nonempty) :
    (s.biUnion t).inf' (Hs.biUnion fun b _ => Ht b) f = s.inf' Hs (fun b => (t b).inf' (Ht b) f) :=
  sup'_biUnion (α := αᵒᵈ) _ Hs Ht

Nonempty Infimum over Union Equals Iterated Nonempty Infimum

Informal description

Let $\beta$ and $\gamma$ be types with decidable equality. Given a nonempty finite set $s \subseteq \gamma$ and a function $t : \gamma \to \mathcal{F}(\beta)$ (where $\mathcal{F}(\beta)$ denotes the type of finite subsets of $\beta$) such that $t(b)$ is nonempty for every $b \in \gamma$, the infimum of $f$ over the union $\bigcup_{x \in s} t(x)$ is equal to the infimum over $s$ of the function $x \mapsto \inf'_{y \in t(x)} f(y)$. In symbols: \[ \inf' \left( \bigcup_{x \in s} t(x) \right) f = \inf'_{x \in s} \left( \inf'_{y \in t(x)} f(y) \right) \] where $\inf'$ denotes the infimum operation restricted to nonempty sets.

Finset.sup_eq_biUnion theorem

{α β} [DecidableEq β] (s : Finset α) (t : α → Finset β) : s.sup t = s.biUnion t

Full source

theorem sup_eq_biUnion {α β} [DecidableEq β] (s : Finset α) (t : α → Finset β) :
    s.sup t = s.biUnion t := by
  ext
  rw [mem_sup, mem_biUnion]

Supremum of Finite Sets Equals Union: $\sup s t = \bigcup_{x \in s} t(x)$

Informal description

For any finite set $s$ of elements of type $\alpha$ and any function $t : \alpha \to \mathcal{F}(\beta)$ (where $\mathcal{F}(\beta)$ denotes the type of finite subsets of $\beta$), the supremum of $t$ over $s$ is equal to the union of the images of $t$ over $s$. In symbols: \[ \sup_{x \in s} t(x) = \bigcup_{x \in s} t(x) \]

TODO