English
Let α be a lattice, s a finite Finset of indices, t i finite sets, and f i : κ i → α. Then the infimum over i ∈ s of the supremum over elements of t i of f i is equal to the supremum over all choices g ∈ ∏ i t i of the infimum over i ∈ s of f i(g(i)).
Русский
Пусть α — решетка, s — конечный множество индексов, t_i — конечные множества, и f_i: κ_i → α. Тогда наименьшее сверху (inf) по i∈s от наибольшего по каждому i элемента из t_i от f_i равняется наибольшему (sup) по всем выборкам g∈∏_i t_i минимальному (inf) по i∈s от f_i(g(i)).
LaTeX
$$$\\inf_{i\\in s} \\bigl(\\sup_{x\\in t(i)} f(i)(x)\\bigr) = \\sup_{g \\in \\prod_{i\\in s} t(i)} \\inf_{i\\in s} f(i)(g(i))$$$
Lean4
theorem inf_sup {κ : ι → Type*} (s : Finset ι) (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → α) :
(s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f _ <| g _ i.2 :=
by
induction s using Finset.induction with
| empty => simp
| insert i s hi ih => ?_
rw [inf_insert, ih, attach_insert, sup_inf_sup]
refine eq_of_forall_ge_iff fun c => ?_
simp only [Finset.sup_le_iff, mem_product, mem_pi, and_imp, Prod.forall, inf_insert, inf_image]
refine
⟨fun h g hg =>
h (g i <| mem_insert_self _ _) (fun j hj => g j <| mem_insert_of_mem hj) (hg _ <| mem_insert_self _ _) fun j hj =>
hg _ <| mem_insert_of_mem hj,
fun h a g ha hg => ?_⟩
-- TODO: This `have` must be named to prevent it being shadowed by the internal `this` in `simpa`
have aux : ∀ j : { x // x ∈ s }, ↑j ≠ i := fun j : s => ne_of_mem_of_not_mem j.2 hi
have :=
h (fun j hj => if hji : j = i then cast (congr_arg κ hji.symm) a else g _ <| mem_of_mem_insert_of_ne hj hji)
(fun j hj => ?_)
· simpa only [cast_eq, dif_pos, Function.comp_def, Subtype.coe_mk, dif_neg, aux] using this
rw [mem_insert] at hj
obtain (rfl | hj) := hj
· simpa
· simpa [ne_of_mem_of_not_mem hj hi] using hg _ _
