csSup_image2_eq_csInf_csSup — Mathlib

English

Given two Galois connections, the two-argument image supremum equals a fixed composition of infima.

Русский

При двух Гало-соединениях верхний предел образа двух аргументов равен фиксированной композиции инфимумов.

LaTeX

$$$(h_1,h_2): s.Nonempty \Rightarrow BddAbove s \Rightarrow t.Nonempty \Rightarrow BddBelow t \Rightarrow sInf (image2 u s t) = u (sInf s) (sInf t)$$$

Lean4

theorem csSup_image2_eq_csInf_csSup (h₁ : ∀ b, GaloisConnection (swap l b ∘ ofDual) (toDual ∘ u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) :
    s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sSup (image2 l s t) = l (sInf s) (sSup t) :=
  csSup_image2_eq_csSup_csSup (α := αᵒᵈ) h₁ h₂

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