English
Assume two families of Galois connections: for all b, GC (swap l b) (u1 b) and for all a, GC (l a) (u2 a). Then the supremum of the image2 construction satisfies sSup(image2 l s t) = l(sSup s)(sSup t).
Русский
Пусть для каждого b выполняется GC (swap l b) (u1 b) и для каждого a — GC (l a) (u2 a). Тогда верхняя граница множества image2 удовлетворяет равенству sSup(image2 l s t) = l(sSup s)(sSup t).
LaTeX
$$$$ (\\forall b,\\; GaloisConnection (swap\\ l\\ b) (u1\\ b)) \\to (\\forall a,\\; GaloisConnection (l\\ a) (u2\\ a)) \\to sSup(image2\\ l\\ s\\ t) = l(sSup\\ s)(sSup\\ t). $$$$
Lean4
theorem sSup_image2_eq_sSup_sSup (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b))
(h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) : sSup (image2 l s t) = l (sSup s) (sSup t) := by
simp_rw [sSup_image2, ← (h₂ _).l_sSup, ← (h₁ _).l_sSup]
