sSup_image2_eq_sInf_sSup — Mathlib

English

Under duality, similar to the previous result, with l swapped and ofDual composition; we obtain sSup(image2 l s t) = l(sSup s)(sInf t) in the dual setting.

Русский

С учетом двойственности аналогично предыдущему, с перестановкой и составлением, получаем равенство в двойственном окружении.

LaTeX

$$$$ sSup(image2\\ l\\ s\\ t) = l(sSup\\ s)(sInf\\ t) \\quad\\text{(в двойственном контексте).} $$$$

Lean4

theorem sSup_image2_eq_sInf_sSup (h₁ : ∀ b, GaloisConnection (swap l b ∘ ofDual) (toDual ∘ u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) : sSup (image2 l s t) = l (sInf s) (sSup t) :=
  sSup_image2_eq_sSup_sSup (α := αᵒᵈ) h₁ h₂

Похожие утверждения