sInf_image2_eq_sInf_sSup — Mathlib

English

Under a pair of GC's, one can express sInf(image2 l s t) as u(sInf s)(sInf t) in the appropriate dual setting.

Русский

При паре связей Галуа можно выразить sInf(image2 l s t) как u(sInf s)(sInf t) в подходящей двойственности.

LaTeX

$$$$ sInf(image2\\ l\\ s\\ t) = u(sInf\\ s)(sInf\\ t). $$$$

Lean4

theorem sInf_image2_eq_sInf_sSup (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
    (h₂ : ∀ a, GaloisConnection (toDual ∘ l₂ a) (u a ∘ ofDual)) : sInf (image2 u s t) = u (sInf s) (sSup t) :=
  sInf_image2_eq_sInf_sInf (β := βᵒᵈ) h₁ h₂

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