English
If h1,h2 provide the appropriate GC's for l1, l2 with swap and ofDual, then sInf(image2 u s t) = u(sInf s)(sInf t).
Русский
Если заданы соответствующие связи Галуа для l1, l2, то sInf(image2 u s t) = u(sInf s)(sInf t).
LaTeX
$$$$ sInf(image2\\ u\\ s\\ t) = u(sInf\\ s)(sInf\\ t). $$$$
Lean4
theorem sInf_image2_eq_sInf_sInf (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
(h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) : sInf (image2 u s t) = u (sInf s) (sInf t) := by
simp_rw [sInf_image2, ← (h₂ _).u_sInf, ← (h₁ _).u_sInf]