csInf_image2_eq_csSup_csSup — Mathlib

English

Given dual Galois connections, the image infimum equals a dual infimum composition.

Русский

С учётом двойственных связей Гало, образ инфимума равен двойственной композиции инфимума.

LaTeX

$$$(h_1 : ∀ b, GaloisConnection (toDual ∘ l_1 b) (swap u b)) (h_2 : ∀ a, GaloisConnection (toDual ∘ l_2 a) (u a)) : s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (image2 u s t) = u (sInf s) (sInf t)$$$

Lean4

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

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