sSup_image2_eq_sInf_sInf — Mathlib

English

Under appropriate GC hypotheses, sSup(image2 l s t) equals l(sInf s)(sInf t).

Русский

При подходящих условиях связи Галуа, sSup(image2 l s t) равно l(sInf s)(sInf t).

LaTeX

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

Lean4

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

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