csSup_image2_eq_csSup_csInf — Mathlib

English

Under suitable dual Galois connections, the two-variable image infimum equals a combination of infima.

Русский

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

LaTeX

$$$[Preorder\alpha][ConditionallyCompleteLattice\beta][ s: Set\alpha][t: Set\beta]\; (h_1)(h_2): s.Nonempty \Rightarrow BddBelow s \Rightarrow t.Nonempty \Rightarrow BddAbove t \Rightarrow sInf (image2 l s t) = l (sInf s) (sInf t)$$$

Lean4

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

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