Lattice operations on finsets of products

This file is concerned with folding binary lattice operations over finsets.

theorem Finset.sup_product_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).sup f = s.sup fun (i : β) => t.sup fun (i' : γ) => f (i, i')

See also Finset.product_biUnion.

theorem Finset.inf_product_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).inf f = s.inf fun (i : β) => t.inf fun (i' : γ) => f (i, i')

theorem Finset.sup_product_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).sup f = t.sup fun (i' : γ) => s.sup fun (i : β) => f (i, i')

theorem Finset.inf_product_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (t : Finset γ) (f : β × γ → α) : (s ×ˢ t).inf f = t.inf fun (i' : γ) => s.inf fun (i : β) => f (i, i')

@[simp]

theorem Finset.sup_prodMap {ι : Type u_6} {κ : Type u_7} {α : Type u_8} {β : Type u_9} [SemilatticeSup α] [SemilatticeSup β] [OrderBot α] [OrderBot β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).sup (Prod.map f g) = (s.sup f, t.sup g)

@[simp]

theorem Finset.inf_prodMap {ι : Type u_6} {κ : Type u_7} {α : Type u_8} {β : Type u_9} [SemilatticeInf α] [SemilatticeInf β] [OrderTop α] [OrderTop β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).inf (Prod.map f g) = (s.inf f, t.inf g)

theorem Finset.sup_inf_sup {α : Type u_1} {ι : Type u_4} {κ : Type u_5} [DistribLattice α] [OrderBot α] (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) : s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun (i : ι × κ) => f i.1 ⊓ g i.2

theorem Finset.inf_sup_inf {α : Type u_1} {ι : Type u_4} {κ : Type u_5} [DistribLattice α] [OrderTop α] (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) : s.inf f ⊔ t.inf g = (s ×ˢ t).inf fun (i : ι × κ) => f i.1 ⊔ g i.2

theorem Finset.sup'_product_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) : (s ×ˢ t).sup' h f = s.sup' ⋯ fun (i : β) => t.sup' ⋯ fun (i' : γ) => f (i, i')

theorem Finset.inf'_product_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeInf α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) : (s ×ˢ t).inf' h f = s.inf' ⋯ fun (i : β) => t.inf' ⋯ fun (i' : γ) => f (i, i')

theorem Finset.sup'_product_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) : (s ×ˢ t).sup' h f = t.sup' ⋯ fun (i' : γ) => s.sup' ⋯ fun (i : β) => f (i, i')

theorem Finset.inf'_product_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeInf α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) : (s ×ˢ t).inf' h f = t.inf' ⋯ fun (i' : γ) => s.inf' ⋯ fun (i : β) => f (i, i')

theorem Finset.prodMk_sup'_sup' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} {β : Type u_9} [SemilatticeSup α] [SemilatticeSup β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s.sup' hs f, t.sup' ht g) = (s ×ˢ t).sup' ⋯ (Prod.map f g)

See also Finset.sup'_prodMap.

theorem Finset.prodMk_inf'_inf' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} {β : Type u_9} [SemilatticeInf α] [SemilatticeInf β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s.inf' hs f, t.inf' ht g) = (s ×ˢ t).inf' ⋯ (Prod.map f g)

See also Finset.inf'_prodMap.

theorem Finset.sup'_prodMap {ι : Type u_6} {κ : Type u_7} {α : Type u_8} {β : Type u_9} [SemilatticeSup α] [SemilatticeSup β] {s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).sup' hst (Prod.map f g) = (s.sup' ⋯ f, t.sup' ⋯ g)

See also Finset.prodMk_sup'_sup'.

theorem Finset.inf'_prodMap {ι : Type u_6} {κ : Type u_7} {α : Type u_8} {β : Type u_9} [SemilatticeInf α] [SemilatticeInf β] {s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).inf' hst (Prod.map f g) = (s.inf' ⋯ f, t.inf' ⋯ g)

See also Finset.prodMk_inf'_inf'.

theorem Finset.sup'_inf_sup' {α : Type u_1} {ι : Type u_4} {κ : Type u_5} [DistribLattice α] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → α) : s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun (i : ι × κ) => f i.1 ⊓ g i.2

theorem Finset.inf'_sup_inf' {α : Type u_1} {ι : Type u_4} {κ : Type u_5} [DistribLattice α] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → α) : s.inf' hs f ⊔ t.inf' ht g = (s ×ˢ t).inf' ⋯ fun (i : ι × κ) => f i.1 ⊔ g i.2