Lattice operations on finsets of functions

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

theorem Finset.inf_sup {α : Type u_1} {ι : Type u_2} [DistribLattice α] [BoundedOrder α] [DecidableEq ι] {κ : ι → Type u_3} (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α) : (s.inf fun (i : ι) => (t i).sup (f i)) = (s.pi t).sup fun (g : (a : ι) → a ∈ s → κ a) => s.attach.inf fun (i : { x : ι // x ∈ s }) => f (↑i) (g ↑i ⋯)

theorem Finset.sup_inf {α : Type u_1} {ι : Type u_2} [DistribLattice α] [BoundedOrder α] [DecidableEq ι] {κ : ι → Type u_3} (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α) : (s.sup fun (i : ι) => (t i).inf (f i)) = (s.pi t).inf fun (g : (a : ι) → a ∈ s → κ a) => s.attach.sup fun (i : { x : ι // x ∈ s }) => f (↑i) (g ↑i ⋯)