sInf_image2_eq_sSup_sInf — Mathlib

English

In the dual setting, with l1 b controlled by swap and ofDual, we have sInf(image2 l s t) = sSup s? or similar dual relation; here stated as a dualized version of the previous identity.

Русский

В двойственном контексте для l1 b, управляемого swap и ofDual, получаем двойственную версию равноcти: sInf(image2 l s t) равняется другой комбинации верхних и нижних пределов.

LaTeX

$$$$ sInf(image2\\ l\\ s\\ t) = sSup(\\text{dual terms}). $$$$

Lean4

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

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