sSup_image2_eq_sSup_sInf — Mathlib

English

Let h1 and h2 express suitable Galois connections (with l and u). Then sSup(image2 l s t) = l(sSup s)(sInf t).

Русский

Пусть заданы подходящие связи Галуа h1, h2 для левых и правых частей, тогда sSup(image2 l s t) = l(sSup s)(sInf t).

LaTeX

$$$$ sSup(image2\\ l\\ s\\ t) = l(sSup\\ s)(sInf\\ t). $$$$

Lean4

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

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