定義 (quiver) とを共にclassとする。 また、に対し、 定義から明らかに、 が成り立つ。 定義 (deductive system) が文脈から明らかな時、をのように省略して書く。の時、定義から だが、これは1-point ruleによって と同値。 定義 (category) 定義 (small c…

定義 (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と読む。 定…

定理 (parameterized infimumとparameterized supremum) ととを全てposetとする。 , . に対するinfimum operatorをと書くとき、に対するinfimum operatorをと書く。 また、に対するsupremum operatorをと書くとき、に対するsupremum operatorをと書く。 証明…

定義 (pseudosemilatticeとcopseudosemilattice) , where . に対し、を、をと書く。 定理 (idempotency) , . 証明 任意のに対し: { -definition } { -definition } { } . 従ってindirect equalityにより。supremumに関しても同様。∎特に、なので、 , . 定理 …

定義 (infimumとsupremum) とを共にposetとする。 Binary relation とをそれぞれ , where で定義し、を、をと読む。 定理 (infimumとsupremumの一意性) . 証明 を仮定する。任意のに対し: { -definition } { -definition } . よって、indirect equalityによ…

以下、とを共にposetとする。 定義 (Galois connection) 定理 (Cancellation) 証明 定義内のととしてそれぞれとを取れば直ちに導かれる。∎ 定義 (Poset of monotonic functions) 定理 (Galois connectionの別の定義) 証明 :Cancellationによりとが成り立つの…