English
Dual statement to Inf-Sup Pi: the supremum over i of the infimum over x in t i of f i x equals the infimum over g in ∏ t i of the supremum over i of f i(g(i)).
Русский
Двойственный к Inf-Sup Pi факт: верхняя граница (sup) по i равна нижней границе (inf) по x из t_i функции f_i(x) и затем инфимуум по выборке g.
LaTeX
$$$\\sup_{i\\in s} \\bigl(\\inf_{x\\in t(i)} f(i)(x)\\bigr) = \\inf_{g \\in \\prod_{i\\in s} t(i)} \\sup_{i\\in s} f(i)(g(i))$$$
Lean4
theorem sup_inf {κ : ι → Type*} (s : Finset ι) (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → α) :
(s.sup fun i => (t i).inf (f i)) = (s.pi t).inf fun g => s.attach.sup fun i => f _ <| g _ i.2 :=
@inf_sup αᵒᵈ _ _ _ _ _ _ _ _
