English
For a monotone g on α×β and directed set d, the upper bounds of g on d equal the upper bounds after restructuring via sprod of fst and snd images.
Русский
Для монотонной функции g на α×β и направленного множества d верхние границы образа равны верхним границам после преобразования через sprod проекций.
LaTeX
$$$ \\text{upperBounds}(\\mathrm{Set.image} g\, d) = \\text{upperBounds}(\\mathrm{Set.image} g\\big(\\mathrm{Set.instSProd.sprod}(\\mathrm{Set.image Prod.fst d}) (\\mathrm{Set.image Prod.snd d})\\big)) $$$
Lean4
theorem upperBounds_image_of_directedOn_prod {γ : Type*} [Preorder γ] {g : α × β → γ} (hg : Monotone g)
{d : Set (α × β)} (hd : DirectedOn (· ≤ ·) d) :
upperBounds (g '' d) = upperBounds (g '' (Prod.fst '' d) ×ˢ (Prod.snd '' d)) :=
le_antisymm (upperBounds_mono_of_isCofinalFor (hd.isCofinalFor_fst_image_prod_snd_image.image_of_monotone hg))
(upperBounds_mono_set (image_mono subset_fst_image_prod_snd_image))
