l_iSup_u — Mathlib

English

In a fully dualized setting, the sInf of the image2 construction equals u applied to the pair of sups: sInf(image2 u s t) = u(sSup s)(sSup t).

Русский

В полностью двойственной обстановке, sInf(image2 u s t) = u(sSup s)(sSup t).

LaTeX

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

Lean4

theorem l_iSup_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → β) :
    l (⨆ i, u (f i)) = ⨆ i, f i :=
  calc
    l (⨆ i : ι, u (f i)) = ⨆ i : ι, l (u (f i)) := gi.gc.l_iSup
    _ = ⨆ i : ι, f i := congr_arg _ <| funext fun i => gi.l_u_eq (f i)

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