sInf_image2_eq_sSup_sSup — Mathlib

English

Under a dual formulation, with l1 b and l2 a, the equality sInf(image2 u s t) = u (sSup s) (sSup t) holds.

Русский

В двойственной формулировке выполняется равенство sInf(image2 u s t) = u(sSup s)(sSup t).

LaTeX

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

Lean4

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

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