次の２つのパッケージの使用例を示します．OCamlの#useの代わりに，HOL Lightのneedsを使うとファイルのリロードが防げます． needs "Library/analysis.ml";; needs "Library/transc.ml";; まずは，チェビシェフの多項式 # let cheb = define `(!x. cheb 0 x…

今回は，任意の集合Aについて，その冪集合2^AからAへの単射が存在しないこと(Cantor)の証明です． 先に示した単射による基数の大小関係の特徴付け # let INJECTIVE_IFF_LEFT_INVERSE = MESON[ MESON`(!a1:A a2:A. f(a1)=f(a2) ==> a1=a2) (!b:B. ?a1:A. !a2:…