Mathlib.Data.Finset.Lattice.Prod

Finset.sup_product_left theorem

(s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).sup f = s.sup fun i => t.sup fun i' => f ⟨i, i'⟩

Full source

/-- See also `Finset.product_biUnion`. -/
theorem sup_product_left (s : Finset β) (t : Finset γ) (f : β × γ → α) :
    (s ×ˢ t).sup f = s.sup fun i => t.sup fun i' => f ⟨i, i'⟩ :=
  eq_of_forall_ge_iff fun a => by simp [@forall_swap _ γ]

Supremum over Product Set Equals Iterated Supremum (Left Version)

Informal description

For any finite sets $s \subseteq \beta$ and $t \subseteq \gamma$, and any function $f : \beta \times \gamma \to \alpha$ where $\alpha$ is a join-semilattice with a bottom element, the supremum of $f$ over the product set $s \times t$ is equal to the supremum over $s$ of the functions that take each $i \in s$ to the supremum over $t$ of the functions $i' \mapsto f(i, i')$. In other words, \[ \sup_{(i,i') \in s \times t} f(i,i') = \sup_{i \in s} \left( \sup_{i' \in t} f(i,i') \right). \]

Finset.sup_product_right theorem

(s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).sup f = t.sup fun i' => s.sup fun i => f ⟨i, i'⟩

Full source

theorem sup_product_right (s : Finset β) (t : Finset γ) (f : β × γ → α) :
    (s ×ˢ t).sup f = t.sup fun i' => s.sup fun i => f ⟨i, i'⟩ := by
  rw [sup_product_left, Finset.sup_comm]

Supremum over Product Set Equals Iterated Supremum (Right Version)

Informal description

For any finite sets $s \subseteq \beta$ and $t \subseteq \gamma$, and any function $f : \beta \times \gamma \to \alpha$ where $\alpha$ is a join-semilattice with a bottom element, the supremum of $f$ over the product set $s \times t$ is equal to the supremum over $t$ of the functions that take each $i' \in t$ to the supremum over $s$ of the functions $i \mapsto f(i, i')$. In other words, \[ \sup_{(i,i') \in s \times t} f(i,i') = \sup_{i' \in t} \left( \sup_{i \in s} f(i,i') \right). \]

Finset.sup_prodMap theorem

 (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : sup (s ×ˢ t) (Prod.map f g) = (sup s f, sup t g)

Full source

@[simp] lemma sup_prodMap (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
    sup (s ×ˢ t) (Prod.map f g) = (sup s f, sup t g) :=
  eq_of_forall_ge_iff fun i ↦ by
    obtain ⟨a, ha⟩ := hs
    obtain ⟨b, hb⟩ := ht
    simp only [Prod.map, Finset.sup_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]
    exact ⟨fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩, by aesop⟩

Supremum of Product Map Equals Pair of Suprema

Informal description

Let $s$ be a nonempty finite set of elements of type $\iota$, and let $t$ be a nonempty finite set of elements of type $\kappa$. Given functions $f : \iota \to \alpha$ and $g : \kappa \to \beta$, where $\alpha$ and $\beta$ are join-semilattices with bottom elements, the supremum of the product map $\text{Prod.map}\, f\, g$ over the product set $s \times t$ is equal to the pair of suprema $(\sup s\, f, \sup t\, g)$. In other words, for nonempty finite sets $s$ and $t$, we have: \[ \sup_{(i,j) \in s \times t} (f(i), g(j)) = \left( \sup_{i \in s} f(i), \sup_{j \in t} g(j) \right). \]

Finset.inf_product_left theorem

(s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).inf f = s.inf fun i => t.inf fun i' => f ⟨i, i'⟩

Full source

theorem inf_product_left (s : Finset β) (t : Finset γ) (f : β × γ → α) :
    (s ×ˢ t).inf f = s.inf fun i => t.inf fun i' => f ⟨i, i'⟩ :=
  @sup_product_left αᵒᵈ _ _ _ _ _ _ _

Infimum over Product Set Equals Iterated Infimum (Left Version)

Informal description

For any finite sets $s \subseteq \beta$ and $t \subseteq \gamma$, and any function $f : \beta \times \gamma \to \alpha$ where $\alpha$ is a meet-semilattice with a top element, the infimum of $f$ over the product set $s \times t$ is equal to the infimum over $s$ of the functions that take each $i \in s$ to the infimum over $t$ of the functions $i' \mapsto f(i, i')$. In other words, \[ \inf_{(i,i') \in s \times t} f(i,i') = \inf_{i \in s} \left( \inf_{i' \in t} f(i,i') \right). \]

Finset.inf_product_right theorem

(s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).inf f = t.inf fun i' => s.inf fun i => f ⟨i, i'⟩

Full source

theorem inf_product_right (s : Finset β) (t : Finset γ) (f : β × γ → α) :
    (s ×ˢ t).inf f = t.inf fun i' => s.inf fun i => f ⟨i, i'⟩ :=
  @sup_product_right αᵒᵈ _ _ _ _ _ _ _

Infimum over Product Set Equals Iterated Infimum (Right Version)

Informal description

For any finite sets $s \subseteq \beta$ and $t \subseteq \gamma$, and any function $f : \beta \times \gamma \to \alpha$ where $\alpha$ is a meet-semilattice with a top element, the infimum of $f$ over the product set $s \times t$ is equal to the infimum over $t$ of the functions that take each $i' \in t$ to the infimum over $s$ of the functions $i \mapsto f(i, i')$. In other words, \[ \inf_{(i,i') \in s \times t} f(i,i') = \inf_{i' \in t} \left( \inf_{i \in s} f(i,i') \right). \]

Finset.inf_prodMap theorem

 (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : inf (s ×ˢ t) (Prod.map f g) = (inf s f, inf t g)

Full source

@[simp] lemma inf_prodMap (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
    inf (s ×ˢ t) (Prod.map f g) = (inf s f, inf t g) :=
  sup_prodMap (α := αᵒᵈ) (β := βᵒᵈ) hs ht _ _

Infimum of Product Map Equals Pair of Infima

Informal description

Let $s$ be a nonempty finite set of elements of type $\iota$, and let $t$ be a nonempty finite set of elements of type $\kappa$. Given functions $f : \iota \to \alpha$ and $g : \kappa \to \beta$, where $\alpha$ and $\beta$ are meet-semilattices with top elements, the infimum of the product map $\text{Prod.map}\, f\, g$ over the product set $s \times t$ is equal to the pair of infima $(\inf s\, f, \inf t\, g)$. In other words, for nonempty finite sets $s$ and $t$, we have: \[ \inf_{(i,j) \in s \times t} (f(i), g(j)) = \left( \inf_{i \in s} f(i), \inf_{j \in t} g(j) \right). \]

Finset.sup_inf_sup theorem

 (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) : s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun i => f i.1 ⊓ g i.2

Full source

theorem sup_inf_sup (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) :
    s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun i => f i.1 ⊓ g i.2 := by
  simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left, sup_product_left]

Distributivity of Meet over Suprema in Product Sets: $(\sup_{i \in s} f(i)) \sqcap (\sup_{j \in t} g(j)) = \sup_{(i,j) \in s \times t} (f(i) \sqcap g(j))$

Informal description

Let $\alpha$ be a distributive lattice with a bottom element, and let $s$ and $t$ be finite sets of elements of types $\iota$ and $\kappa$ respectively. For any functions $f \colon \iota \to \alpha$ and $g \colon \kappa \to \alpha$, the meet of the suprema $\sup_{i \in s} f(i)$ and $\sup_{j \in t} g(j)$ is equal to the supremum over the product set $s \times t$ of the meets $f(i) \sqcap g(j)$. In symbols: \[ \left( \sup_{i \in s} f(i) \right) \sqcap \left( \sup_{j \in t} g(j) \right) = \sup_{(i,j) \in s \times t} \left( f(i) \sqcap g(j) \right). \]

Finset.inf_sup_inf theorem

 (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) : s.inf f ⊔ t.inf g = (s ×ˢ t).inf fun i => f i.1 ⊔ g i.2

Full source

theorem inf_sup_inf (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) :
    s.inf f ⊔ t.inf g = (s ×ˢ t).inf fun i => f i.1 ⊔ g i.2 :=
  @sup_inf_sup αᵒᵈ _ _ _ _ _ _ _ _

Distributivity of Join over Infima in Product Sets: $(\inf_{i \in s} f(i)) \sqcup (\inf_{j \in t} g(j)) = \inf_{(i,j) \in s \times t} (f(i) \sqcup g(j))$

Informal description

Let $\alpha$ be a distributive lattice with a top element, and let $s$ and $t$ be finite sets of elements of types $\iota$ and $\kappa$ respectively. For any functions $f \colon \iota \to \alpha$ and $g \colon \kappa \to \alpha$, the join of the infima $\inf_{i \in s} f(i)$ and $\inf_{j \in t} g(j)$ is equal to the infimum over the product set $s \times t$ of the joins $f(i) \sqcup g(j)$. In symbols: \[ \left( \inf_{i \in s} f(i) \right) \sqcup \left( \inf_{j \in t} g(j) \right) = \inf_{(i,j) \in s \times t} \left( f(i) \sqcup g(j) \right). \]

Finset.sup'_product_left theorem

 {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
  (s ×ˢ t).sup' h f = s.sup' h.fst fun i => t.sup' h.snd fun i' => f ⟨i, i'⟩

Full source

theorem sup'_product_left {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
    (s ×ˢ t).sup' h f = s.sup' h.fst fun i => t.sup' h.snd fun i' => f ⟨i, i'⟩ :=
  eq_of_forall_ge_iff fun a => by simp [@forall_swap _ γ]

Supremum over product set equals iterated supremum (left version)

Informal description

Let $s$ be a finite set of elements of type $\beta$, $t$ a finite set of elements of type $\gamma$, and $f : \beta \times \gamma \to \alpha$ a function where $\alpha$ is a join-semilattice. If the product set $s \times t$ is nonempty (with proof $h$), then the supremum of $f$ over $s \times t$ equals the supremum over $s$ of the functions that take each $i \in s$ to the supremum over $t$ of the functions $i' \mapsto f(i, i')$. In symbols: $$ \sup'_{s \times t} f = \sup'_s \left( \lambda i, \sup'_t (\lambda i', f(i, i')) \right) $$

Finset.sup'_product_right theorem

 {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
  (s ×ˢ t).sup' h f = t.sup' h.snd fun i' => s.sup' h.fst fun i => f ⟨i, i'⟩

Full source

theorem sup'_product_right {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
    (s ×ˢ t).sup' h f = t.sup' h.snd fun i' => s.sup' h.fst fun i => f ⟨i, i'⟩ := by
  rw [sup'_product_left, Finset.sup'_comm]

Supremum over product set equals iterated supremum (right version)

Informal description

Let $s$ be a finite set of elements of type $\beta$, $t$ a finite set of elements of type $\gamma$, and $f : \beta \times \gamma \to \alpha$ a function where $\alpha$ is a join-semilattice. If the product set $s \times t$ is nonempty (with proof $h$), then the supremum of $f$ over $s \times t$ equals the supremum over $t$ of the functions that take each $i' \in t$ to the supremum over $s$ of the functions $i \mapsto f(i, i')$. In symbols: $$ \sup'_{s \times t} f = \sup'_t \left( \lambda i', \sup'_s (\lambda i, f(i, i')) \right) $$

Finset.prodMk_sup'_sup' theorem

 (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
  (sup' s hs f, sup' t ht g) = sup' (s ×ˢ t) (hs.product ht) (Prod.map f g)

Full source

/-- See also `Finset.sup'_prodMap`. -/
lemma prodMk_sup'_sup' (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
    (sup' s hs f, sup' t ht g) = sup' (s ×ˢ t) (hs.product ht) (Prod.map f g) :=
  eq_of_forall_ge_iff fun i ↦ by
    obtain ⟨a, ha⟩ := hs
    obtain ⟨b, hb⟩ := ht
    simp only [Prod.map, sup'_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]
    exact ⟨by aesop, fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩⟩

Supremum of Product Map Equals Pair of Suprema

Informal description

Let $s$ be a nonempty finite set of elements of type $\iota$, $t$ a nonempty finite set of elements of type $\kappa$, and $f : \iota \to \alpha$, $g : \kappa \to \beta$ functions where $\alpha$ and $\beta$ are join-semilattices. Then the pair of suprema $(\sup' s \, f, \sup' t \, g)$ equals the supremum of the product map $\text{Prod.map}\, f\, g$ over the product set $s \times t$. In symbols: $$ \left(\sup'_{i \in s} f(i), \sup'_{j \in t} g(j)\right) = \sup'_{(i,j) \in s \times t} (f(i), g(j)) $$

Finset.sup'_prodMap theorem

 (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) :
  sup' (s ×ˢ t) hst (Prod.map f g) = (sup' s hst.fst f, sup' t hst.snd g)

Full source

/-- See also `Finset.prodMk_sup'_sup'`. -/
-- @[simp] -- TODO: Why does `Prod.map_apply` simplify the LHS?
lemma sup'_prodMap (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) :
    sup' (s ×ˢ t) hst (Prod.map f g) = (sup' s hst.fst f, sup' t hst.snd g) :=
  (prodMk_sup'_sup' _ _ _ _).symm

Supremum of Product Map Equals Pair of Suprema (Generalized Version)

Informal description

Let $s$ be a finite set of elements of type $\iota$, $t$ a finite set of elements of type $\kappa$, and $f : \iota \to \alpha$, $g : \kappa \to \beta$ functions where $\alpha$ and $\beta$ are join-semilattices. If the product set $s \times t$ is nonempty (with proof $hst$), then the supremum of the product map $\text{Prod.map}\, f\, g$ over $s \times t$ equals the pair of suprema $(\sup' s \, f, \sup' t \, g)$. In symbols: $$ \sup'_{s \times t} (f \times g) = \left(\sup'_s f, \sup'_t g\right) $$

Finset.inf'_product_left theorem

 {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
  (s ×ˢ t).inf' h f = s.inf' h.fst fun i => t.inf' h.snd fun i' => f ⟨i, i'⟩

Full source

theorem inf'_product_left {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
    (s ×ˢ t).inf' h f = s.inf' h.fst fun i => t.inf' h.snd fun i' => f ⟨i, i'⟩ :=
  sup'_product_left (α := αᵒᵈ) h f

Infimum over product set equals iterated infimum (left version)

Informal description

Let $s$ be a finite set of elements of type $\beta$, $t$ a finite set of elements of type $\gamma$, and $f : \beta \times \gamma \to \alpha$ a function where $\alpha$ is a meet-semilattice. If the product set $s \times t$ is nonempty (with proof $h$), then the infimum of $f$ over $s \times t$ equals the infimum over $s$ of the functions that take each $i \in s$ to the infimum over $t$ of the functions $i' \mapsto f(i, i')$. In symbols: $$ \inf'_{s \times t} f = \inf'_s \left( \lambda i, \inf'_t (\lambda i', f(i, i')) \right) $$

Finset.inf'_product_right theorem

 {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
  (s ×ˢ t).inf' h f = t.inf' h.snd fun i' => s.inf' h.fst fun i => f ⟨i, i'⟩

Full source

theorem inf'_product_right {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
    (s ×ˢ t).inf' h f = t.inf' h.snd fun i' => s.inf' h.fst fun i => f ⟨i, i'⟩ :=
  sup'_product_right (α := αᵒᵈ) h f

Infimum over product set equals iterated infimum (right version)

Informal description

Let $s$ be a finite set of elements of type $\beta$, $t$ a finite set of elements of type $\gamma$, and $f : \beta \times \gamma \to \alpha$ a function where $\alpha$ is a meet-semilattice. If the product set $s \times t$ is nonempty (with proof $h$), then the infimum of $f$ over $s \times t$ equals the infimum over $t$ of the functions that take each $i' \in t$ to the infimum over $s$ of the functions $i \mapsto f(i, i')$. In symbols: $$ \inf'_{s \times t} f = \inf'_t \left( \lambda i', \inf'_s (\lambda i, f(i, i')) \right) $$

Finset.prodMk_inf'_inf' theorem

 (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
  (inf' s hs f, inf' t ht g) = inf' (s ×ˢ t) (hs.product ht) (Prod.map f g)

Full source

/-- See also `Finset.inf'_prodMap`. -/
lemma prodMk_inf'_inf' (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
    (inf' s hs f, inf' t ht g) = inf' (s ×ˢ t) (hs.product ht) (Prod.map f g) :=
  prodMk_sup'_sup' (α := αᵒᵈ) (β := βᵒᵈ) hs ht _ _

Infimum of Product Map Equals Pair of Infima

Informal description

Let $s$ be a nonempty finite set of elements of type $\iota$, $t$ a nonempty finite set of elements of type $\kappa$, and $f \colon \iota \to \alpha$, $g \colon \kappa \to \beta$ functions where $\alpha$ and $\beta$ are meet-semilattices. Then the pair of infima $(\inf' s\, f, \inf' t\, g)$ equals the infimum of the product map $\text{Prod.map}\, f\, g$ over the product set $s \times t$. In symbols: $$ \left(\inf'_{i \in s} f(i), \inf'_{j \in t} g(j)\right) = \inf'_{(i,j) \in s \times t} (f(i), g(j)) $$

Finset.inf'_prodMap theorem

 (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) :
  inf' (s ×ˢ t) hst (Prod.map f g) = (inf' s hst.fst f, inf' t hst.snd g)

Full source

/-- See also `Finset.prodMk_inf'_inf'`. -/
-- @[simp] -- TODO: Why does `Prod.map_apply` simplify the LHS?
lemma inf'_prodMap (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) :
    inf' (s ×ˢ t) hst (Prod.map f g) = (inf' s hst.fst f, inf' t hst.snd g) :=
  (prodMk_inf'_inf' _ _ _ _).symm

Infimum of Product Map Equals Pair of Infima

Informal description

Let $s$ be a finite set of elements of type $\iota$, $t$ a finite set of elements of type $\kappa$, and $f \colon \iota \to \alpha$, $g \colon \kappa \to \beta$ functions where $\alpha$ and $\beta$ are meet-semilattices. If the product set $s \times t$ is nonempty (with proof $hst$), then the infimum of the product map $\text{Prod.map}\, f\, g$ over $s \times t$ equals the pair of infima $(\inf' s\, f, \inf' t\, g)$. In symbols: $$ \inf'_{s \times t} (\text{Prod.map}\, f\, g) = \left(\inf'_s f, \inf'_t g\right) $$

Finset.sup'_inf_sup' theorem

 (f : ι → α) (g : κ → α) : s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' (hs.product ht) fun i => f i.1 ⊓ g i.2

Full source

theorem sup'_inf_sup' (f : ι → α) (g : κ → α) :
    s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' (hs.product ht) fun i => f i.1 ⊓ g i.2 := by
  simp_rw [Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left, sup'_product_left]

Distributivity of Meet over Finite Suprema in Product Sets: $(\sup' s\, f) \sqcap (\sup' t\, g) = \sup'_{s \times t} (f \sqcap g)$

Informal description

Let $\alpha$ be a distributive lattice, $s$ a nonempty finite set of elements of type $\iota$, $t$ a nonempty finite set of elements of type $\kappa$, and $f \colon \iota \to \alpha$, $g \colon \kappa \to \alpha$ functions. Then the meet of the suprema $\sup' s\, f$ and $\sup' t\, g$ equals the supremum over the product set $s \times t$ of the functions $(i,j) \mapsto f(i) \sqcap g(j)$. In symbols: $$ \left(\sup'_{i \in s} f(i)\right) \sqcap \left(\sup'_{j \in t} g(j)\right) = \sup'_{(i,j) \in s \times t} \left(f(i) \sqcap g(j)\right) $$

Finset.inf'_sup_inf' theorem

 (f : ι → α) (g : κ → α) : s.inf' hs f ⊔ t.inf' ht g = (s ×ˢ t).inf' (hs.product ht) fun i => f i.1 ⊔ g i.2

Full source

theorem inf'_sup_inf' (f : ι → α) (g : κ → α) :
    s.inf' hs f ⊔ t.inf' ht g = (s ×ˢ t).inf' (hs.product ht) fun i => f i.1 ⊔ g i.2 :=
  @sup'_inf_sup' αᵒᵈ _ _ _ _ _ hs ht _ _

Distributivity of Join over Finite Infima in Product Sets: $(\inf' s\, f) \sqcup (\inf' t\, g) = \inf'_{s \times t} (f \sqcup g)$

Informal description

Let $\alpha$ be a distributive lattice, $s$ a nonempty finite set of elements of type $\iota$, $t$ a nonempty finite set of elements of type $\kappa$, and $f \colon \iota \to \alpha$, $g \colon \kappa \to \alpha$ functions. Then the join of the infima $\inf' s\, f$ and $\inf' t\, g$ equals the infimum over the product set $s \times t$ of the functions $(i,j) \mapsto f(i) \sqcup g(j)$. In symbols: $$ \left(\inf'_{i \in s} f(i)\right) \sqcup \left(\inf'_{j \in t} g(j)\right) = \inf'_{(i,j) \in s \times t} \left(f(i) \sqcup g(j)\right) $$