定義 (constant combinator) 集合とに対し、関数を で定義する。 定理 とが共にposetの時、 . 証明 を固定すると、任意のに対し: { -definition } { right zero of } . よって. さらに、任意のに対し: { lifting + -definition } { -introduction } . よって…

定義 (semilatticeとcosemilattice) , . 定理 (topとbottom) , . 証明 { definition } { 1-point: } { lifting + empty range } . least elementに関しても同様。∎の時のgreatest element を、の時のleast element をと書き、それぞれtopとbottomと読む。 定…