https://www.youtube.com/watch?v=QI-fEXSX1BA 2分30秒くらい progress has been super-slow. 進捗は非常に遅い、と。https://leanprover.github.io/talks/vu2019.pdf P.9 ： Connection between modules, packages, and namespaces in Lean 3 is not very c…

leanprover/lean4:stable と leanprover/lean4:v4.0.0-m5 という名前のツールチェーンは同じもので、名前だけが違う。どちらも、https://github.com/leanprover/lean4/releases/expanded_assets/v4.0.0-m5 からダウンロードされる。が、elanはそれに気付かず…

git ls-files --stage と git ls-files --cached は同じファイルをリストする。表示が違うだけ。 git ls-files --cached ファイル名だけ git ls-files --stage ファイル名以外に、オブジェクトID、ステージ数〈staging number〉、モード ホントにダメなコマ…

図のタイトルをYAMLフロントマターにするのは使えねー。 統一性がない。 構文： flowchart sequence diag. ID[ラベル] タイプ ID as ラベル ソース アロー ラベル ターゲット ソース アロー ターゲット: ラベル 次のようにすれば、統一的だった。 ノードは …

Objectはオブジェクト型だけでなくて、ボクシングしてオブジェクトになるものも含まれる。null以外なんでもいい。{} が Object と同義なのは、どうかしている。object は {[key: (string|number)] : any} と同義かな？ たぶん。いずれにしても整合性がない。

flowchart と subgraph の構文が一致しない。flowchart id[title] direction TB なら良かった。 辺へのスタイリングが番号指定でカス

ESModules を使ったソースで、ts-node hoge.mts すると、ts-node が次のエラーを出す。 SyntaxError: Cannot use import statement outside a moduleファイル名が .mts 拡張子なので、"type": "module" 要らないはずだが、package.json に次を入れてみた。 "…

何日か前に評判になったブログ記事： http​://hants.livedoor.biz/archives/52184019.html 2021年09月28日 梅澤愛優香さんに対する、はんつ遠藤の意見 体に染み付いた醜悪なオジサン構文の事例。 出だしの挨拶「お世話になっております。」 最後の挨拶「お疲…

Leanの推論規則 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。https://leanprover.github.io/logic_and_proof/nd_quickref.html に自然演繹のまとめがある。それに従うが、双含意〈bi-inplication〉は除く。 論理記号 導入 消去 Implication ラムダ抽象…

マトリックス全体の列間寸法、行間寸法を調整する以外にアローの長さは調整できない。アローごと、行ごと、列ごとの調整は不可能。

構文解析がXyJax側で行われるので、newcommandで定義されたマクロは効かない。TeXコードを入れたブロック内はTeX側に移譲して構文解析するからマクロが効く。複雑な組み合わせを繰り返し使うから、マクロが効かないのは辛い。

rw h は等式的法則 h （hは等式的法則のラベル）を使ってターゲット内の項を別な項で置き換える。 rw ←h とすると、a=>b 方向のリライトをする。矢印が逆！ rw h とすると、a まったく！

https://leanprover.github.io/reference/tactics.html#basic-tactics This tactic applies to a goal whose goal has the form t ~ u where ~ is a reflexive relation, この言い回しにはさんざん悩まされた。「ゴール」に意味が。 証明状態 メインゴール …

区別しない習慣が悪い癖。 連言リストと選言リストの区別 連言リストと選言リストは明確に分かるようにする。 連言リスト ∧(A, B, C) 選言リスト ∨(A, B, C) または、 連言リスト (A, B, C) 選言リスト (A | B | C) 単元リストと空リストのとき区別できない…

ゴールズ状態にはカーソルがあって、現ゴールが決まっている。それは表示上の一番上または一番左のゴールで、アタック（タクティクの適用）は常に現ゴールに対して行われる。したがって、逆リーズニングツリーを上から下、左から右に描けば、上から下の方向…

コンテキスト内のセットアップではない型宣言を仮説〈hypothesis〉と呼ぶ。ラムダリスト内の型宣言を仮定〈assumption〉と呼ぶ。だが、仮説によりターゲットが直接得られるときにう使うタクティク名は premise, hypothesis ではなくて、asspumption （by ass…

sumii先生情報： > 「2x」や「x^2」は「多項式」ではない、 知りませんでした。確かに謎ですね。

正確には：

やはり、プレテーブルとテーブルを区別しないのはダメだ。プレテーブルでは実体集合の概念が入っており、プレテーブルの域は実体集合であり、カラムが候補キーであるか判断できる。 テーブルは、実体集合はなくなり、タプル集合となる。タプル集合（これが《…

教科書:コース→書籍 の図 digraph { /* 実体集合 */ コース 書籍 /* 関連 */ コース -> 書籍 [label="教科書"] } 多値写像'教科書'のグラフ集合を Graph(多値写像) として、射影写像を first, second と書くとして： digraph { /* 集合 */ G[label="Graph(教…

これはER図に限ったことではないが、A⊆X をどう図示するか？ 埋め込み写像 i:A→X 1からの多値写像（非決定性要素） A:1→X 集合としてのA digraph{ /* 集合 */ A X /* 写像 */ A -> X[label="i"] /* 埋め込み */ X1[label="X"] 1[label="{0}"] 1 -> X1[label=…

とりあえず、Graphvizソース、必要があればレンダリングして見る。ER図は視点によって変わってしまう。どれがいいかの判断ができないし、相互変換も難しい。学生中心に見ると： digraph{ /* ドメイン */ D_氏名[shape=none,fontcolor=red] D_年齢[shape=none…

過去： 代表値汎関数とシャープ化オペレータ - (新) 檜山正幸のキマイラ飼育記 メモ編 ジリィ型モナドのアイレンベルク／ムーア代数を{重心 | 平均{値}? | 中心 | 代表{値}}代数と呼ぶ。その代数の代数演算、または代数演算の結果を{重心 | 平均{値}? | 中心…

確率変数（または変量）は、確率分布＝確率測度＝確率空間＝ランダム要素 だと解釈できる。例題で「泥棒が入る事象」「地震が起きる事象」などと言っている。この「事象」は国語辞典的な「事態・事件」の意味。因果グラフのノードなので、「泥棒が入る確率変…

hrタグを直接入れるとき、表示が変わる。一番多く使っていた「前後空行なし改行」が隙間が空くので、修正している。以前は、隙間は開かなかった。 前後空行なし改行 段落。 <hr> 段落。 段落。 段落。 前後空行あり改行 段落。 <hr> 段落。 段落。段落。 空行なし後</hr></hr>…

以前は、preのなかの改行はそのまま保持されたが、&ltbr>が行末に付加される仕様となった。 以前、preを使っていたところがスカスカ。 pre記法に直せばスカスカは直るが、CSSクラスとCSSでスタイリングしていたのが無効になってしまう。 hand-calc, proof, o…

以前は、tex記法内に二重の丸括弧が出てきても反応しなかったのが、反応するようになってしまった。

行の銭湯にある「|-」に反応するようになってしまった。よって、証明可能性記号が行頭で使えない。過去記事は壊れる。

圏論の随伴とメイト理論を使った線形代数。双対性はコンパクト閉圏のなかで定式化する。背後には2-圏論。 線形代数 メイト理論 ベクトル空間 関手 双対空間ペア 随伴関手ペア 双対パートナー空間 随伴パートナー関手 余評価 単位 評価 余単位 双対メイト 随…

反変ベクトルと共変ベクトル -- これはイカンわ、ダメなヤツだわ。因習的微分幾何や物理で出てくるヤツ。まったく分からんヤツ。とりあえずは、特定のベクトル空間Vに対して、Vの要素が反変ベクトル、Vの双対空間の要素が共変ベクトル。が、ベクトル空間はフ…