English
Given certain Galois connections, the supremum of the two-variable image equals a conjunction of sups.
Русский
При задании соответствующих связей Гало-соединений, верхняя грань образа двух переменных равна сочетанию верхних пределов.
LaTeX
$$$[Preorder\alpha][ConditionallyCompleteLattice\beta][
s: Set\alpha][t: Set\beta]\; (l:u)\;(u₁,u₂) : \text{csSup image2 } l s t = l (sSup s) (sSup t)$$$
Lean4
theorem csSup_image2_eq_csSup_csSup (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b))
(h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty)
(ht₁ : BddAbove t) : sSup (image2 l s t) = l (sSup s) (sSup t) :=
by
refine eq_of_forall_ge_iff fun c => ?_
rw [csSup_le_iff (hs₁.image2 (fun _ => (h₁ _).monotone_l) (fun _ => (h₂ _).monotone_l) ht₁) (hs₀.image2 ht₀),
forall_mem_image2, forall₂_swap, (h₂ _).le_iff_le, csSup_le_iff ht₁ ht₀]
simp_rw [← (h₂ _).le_iff_le, (h₁ _).le_iff_le, csSup_le_iff hs₁ hs₀]
