補題
G を可換束群(過去スレ009の761)とする。
(x_i), i ∈ I を G の元の族で x = sup {x_i; i ∈ I} が存在するとする。
y を G の任意の元とする。
このとき inf(x, y) = sup {inf(x_i, y) ; i ∈ I} である。
証明
任意の i ∈ I に対して inf(x_i, y) = y + inf(x_i - y, 0)
よって、
sup {inf(x_i, y) ; i ∈ I} = y + sup {inf(x_i - y, 0) ; i ∈ I}
一方、
>>2 より、
sup {inf(x_i - y, 0) ; i ∈ I} = inf(x - y, 0)
よって、
sup {inf(x_i, y) ; i ∈ I} = y + inf(x - y, 0) = inf(x, y)
証明終