csInf_image2_eq_csSup_csInf — Mathlib

English

Under two Galois connections, the image infimum equals an infimum-infimum composition.

Русский

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

LaTeX

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

Lean4

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

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