$`x = f(x)`$ $`x \ne f(x)`$ これの解釈： $`\forall x\in X.\, x = f(x)`$ $`\exists x\in X.\, x = f(x)`$ $`\forall x\in X.\, x \ne f(x)`$ $`\exists x\in X.\, x \ne f(x)`$ 関数レベルでの等式： $`\mathrm{id}_X = f`$ $`\mathrm{id}_X \ne f`$

米田埋め込み的なもの 米田単元埋め込み $`a \mapsto \{a\}`$ 米田クロネッカー・デルタ $`a\mapsto \delta^a`$ 米田CPS変換 $`f \mapsto f^*`$ 米田ケーリー表現／米田ケーリー加群 米田エルブラン・モデル 淡中埋め込み的なもの 淡中単項フィルター 淡中ゲ…

http://webdam.inria.fr/Alice/pdfs/Chapter-8.pdf より。Movieテーブル title Director Actor Showing〈上映〉テーブル theater screen title snack ： 提供しているスナック（飲料と軽食） 昔は2本立てがあったが、今はほぼない。以前から使っている。学生…

Title: Kalish/Montague and Ja´skowski Natural Deduction Authors: Mohammad M. Ajallooeian, Francis Jeffry Pelletier Pages: 9p URL: https://mirror.las.iastate.edu/tex-archive/macros/latex/contrib/natded/extended_doc.pdf $`\newcommand{\mrm}[1…

Title: A Browsable Format for Proof Presentation Date: June 1996 Authors: Jim Grundy, Turku Centre Pages: 8p URL: https://www.researchgate.net/publication/2359706_A_Browsable_Format_for_Proof_Presentation structured calculational proof に…

def FooRetType (b:Bool) : Type := match b with | false => Nat | true => String def foo (b: Bool) : FooRetType b := match b with | false => (1 : Nat) | true => "hello" #eval foo true #eval foo false

theorem half_DeMorgan premise h: ￢A∧￢B entails ￢(A∨B) proof we have not_a: ￢A by using And_left with h we have not_b: ￢B by using And_light with h we conclude ￢(A ∨ B) by using Or_tuple with not_a and not_b end 定理 ド・モルガンの半…

数学的帰納法のステップの部分。 section NatInd def sumto (n : Nat) : Nat := match n with | Nat.zero => 0 | Nat.succ m => (sumto m) + (Nat.succ m) def arith (n : Nat) : Nat := (n * (n + 1))/2 -- theorem target 跡地 theorem case_zero : sumto …

rflは exact Eq.refl 項 の略記。適切な項は見つけてくれる。 theorem t1 (y : Nat) : (fun x : Nat => 0) y = 0 := by rfl theorem t2 (y : Nat) : (fun x : Nat => 0) y = 0 := by exact Eq.refl 0A = A の形でないとターゲットに適用できない。カーネルに…

/-- 自然数に関する帰納原理 -/ theorem NatIndPrinciple (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (Nat.succ n)) : ∀ n, p n := by intro n cases n · exact hz · apply hs /-- 自然数に関する帰納原理を with付きで書いてみる -/ theorem NatIndPrincipl…

def Obj := Type def Enricher := Type def Hom (α β : Obj) : Enricher := (α → β) structure EndoFunctor where obj : Obj → Obj -- 台型構成子＝対象パート hom : {α β : Obj} → (Hom α β) → (Hom (obj α) (obj β)) -- ホムパート #check @EndoFunctor.ho…

スキーマ、タプル空間、タプルインスタンス、フィールド関数、テーブル structure Schema where fields : Type typeAssig : fields → Type def TupleSpace (S : Schema) := ((f : S.fields) → S.typeAssig f) inductive NameAge where | name : NameAge | ag…

http://www.omdoc.org/pubs/omdoc1.2.pdf の印刷ページ21（p.37）から：Definition 3.2.5 (Monoid) A monoid is a semigroup $`S = (G, \circ)`$ with an element $`e\in G`$, such that $`e ◦ x = x`$ for all $`x ∈ G`$. $`e`$ is called a left unit of $…

theorem ext {a b : Set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) : a = b := funext (fun x ↦ propext (h x))事実 半形式的：$`\text{Fact ext}\\ \text{For } a, b : \mathrm{Set}\: \alpha \\ \text{When } \forall (x : α),\, x \in a \iff x \in b \\ \text{…

$`\require{color} % 緑色 \newcommand{\In}{ \text{ in }} \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } } % 使用 \newcommand{\Let}{\Keyword{Let } }% 使用 \newco…

structure PreOrder where U : Type le : U → U → Prop le_refl : ∀(x : U), le x x le_trans : ∀(x y z: U), (le x y ∧ le y z) → le x z inductive ab where | a | b def ab_le (x : ab) (y : ab) : Prop := match (x, y) with | (.a, _) => True | (.b, .…

def f1 : Nat → Nat → Nat := by exact (fun (n m: Nat) => n + m) #check f1 def f2 (n: Nat): Nat → Nat := by intro m exact n + m #check f2 def f3 (n m: Nat): Nat := by exact n + m #check f3

これって、昔Catyでやろうとしていたこと（一部はやった）ことだ。 structure LatticePoint2D where x: Int y: Int #check LatticePoint2D def LatticePoint2D.moveBy (p : LatticePoint2D) (u v:Int) : LatticePoint2D := { x := p.x + u y := p.y + v } #c…

次のパッケージをトップレベルパッケージ（依存パッケージではなく）git clone でインストールする。 "leancolls" : https://github.com/jamesgallicchio/leancolls インストールしてすぐ気がつくのは： ./lean_packages/ というディレクトリがある。./lake-…

variable (α : Type) variable (F G : α → Type) def f : (∀ x : α, F x × G x) → (∀ y : α, F y) := fun h : ∀ x : α, F x × G x => fun y : α => (h y).fst関数ヘッドを変形すると： variable (α : Type) variable (F G : α → Type) def f' (h : ∀ x : α, …

演算子優先度〈prec〉は適切かどうかわからない。 infix:70 "←" => Nat.pow #eval 5 ← 2 -- 25 def sqPow (n:Nat) : Nat := n ← (n * n) #eval sqPow 2 -- 16

$`\newcommand{\cat}[1]{ \mathcal{#1}} %`$>コアージョングラフは、有向グラフとしての $`\cat{C}`$ の[/単純/な/部分グラフ]である。コアージョングラフ $`G`$ は単純グラフなので、射の両端 $`X, Y`$ が決まれば、射があればそれは一意的に決まる。その射…

PRel = PolyRel を使う。 名付け〈naming | identification | {一意}?識別〉は多関係のなかで単射写像になるもの。PRel(I → X|injective) トリプルは、PRel(P → S, O| function) の要素〈多射〉の要素〈レコード〉 他に、PRel(P → S, O, O'|function) とかも…

形態： article, paper, online-book, blogPost 言語: 日本語, 英語 話題： onBlog, onEnglish, onBook 品詞： 名詞、形容詞、動詞（言葉へのタギング） 書評と、アマゾンの本のページと、オンラインブックに book というタグが付く可能性がある。タギングは…

目次の木構造を反映させる。 ベクトル空間 <ベクトル空間序> ベクトル空間の公理 <公理> ベクトル空間の実例 <実例> 基底 基底の定義 次元 (次元の一意性定理) <次元一意性> 有限次元ベクトル空間useは内部的に解決されているから露出させない。デンドログラ…

目次： 1. ベクトル空間 <ベクトル空間序> 1.1. ベクトル空間の公理 <公理> 1.2. ベクトル空間の実例 <実例> 2. 基底 2.1 基底の定義 2.2 次元 (次元の一意性定理) <次元一意性> 2.2 有限次元ベクトル空間用語： ベクトル空間 -(has_alias)-> 線形空間 ベク…

win10 |- windows html5 |- html es6 |- js js |- proglang proglang |- software js ⇔ javascript

gitの誤認例：.gitignore, --squash - (新) 檜山正幸のキマイラ飼育記 メモ編 にて： 今まで、変な説明を見ても記録しなかったが、これからは記録に残そう。 https://qiita.com/ryosuketter/items/a6047b0270ea999fd51b 今回は、ステージングエリアから、ワ…

gitのキャッシュ？ ステージ？ インデックス？ - (新) 檜山正幸のキマイラ飼育記 メモ編 を書いたキッカケは： https://zenn.dev/unemployed/articles/git-github-team 「間違えてアップしたファイルを.gitignoreで削除する方法」という記述がある。どうも、…

アリーナ1 {旅行 → {1日目, 2日目, 3日目}} $`y^3`$ アリーナ2 {和 → {焼き魚, 煮魚, 刺し身}, 洋 → {グリルチキン}, 中華 → {エビチリ, 麻婆豆腐}} $`y^3 + y + y^2`$ アリーナ3 {和 → {羊羹, わらび餅}, 洋 → {ショートケーキ, モンブラン, ババロア}} $`y…