csInf_image2_eq_csInf_csSup — Mathlib

English

If certain Galois connections hold, then the two-variable image infimum equals a supremum-infimum mixture of the bounds.

Русский

При выполнении некоторых Гало-соединений образ2 равен смеси верхних и нижних пределов.

LaTeX

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

Lean4

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

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