← ファイル一覧
（保存にはログインが要ります）
1_basis/3.book
ヘッダ
行番号
title 記述にクラスを使用した定理 author admin import 2_class
section 演算に関する定理 word + txt 一般結合則について少し厳密に述べてみます。 !let goal := `[ a ; b col ∈_ \{ cls x | [ ∀ y ; z \; x + (y + z) = (x + y) + z ] \} ] ⟹ a + (b + (y + z)) = ((a + b) + y) + z` thm goal -| O prf goal p-| O; br txt 演算の中心について。`+` が結合的なら、可換なものどうしの和もまた可換です。 !let goal := `[ ∀ u ; v ; w \; u + (v + w) = (u + v) + w ] ⟹ ([ a ; b col ∈_ \{ cls x | ∀ y \, x + y = y + x \} ] ⟹ a + b ∈_ \{ cls x | ∀ y \, x + y = y + x \})` thm goal -| O prf goal p-| O; br let |C_ := `\{ cls x | ∀ y \, x + y = y + x \}` !let goal := `[ ∀ u ; v ; w \; u + (v + w) = (u + v) + w ] ⟹ [ a ; b col ∈_ |C_ ] ⇒ a + b ∈_ |C_` thm goal -| O prf goal p-| O; section 関係に関する定理 br txt 関係そのものの性質も word で書けます。関係は `[ ]` で引用して渡します。 word :R :T :X txt `[..p^] :R` は反射律 `∀ x \, x ..p^ x`、`[..p^] :T` は推移律、`[..p^] :X` は対称律です。 txt 関係そのものは `|..p^` のような ..v^-Form で書きます(この類は紹介されません)。 txt 同値関係のとき「関係すること」は「クラスが等しいこと」で言い換えられます。 !let goal := `([|..p^] :R and [|..p^] :T and [|..p^] :X) ⟹ (a |..p^ b ⟺ \{ cls x | x |..p^ a \} =_ \{ cls x | x |..p^ b \})` thm goal -| O prf goal p-| O; br txt 順序のような関係でも、クラスにすると言えることがあります。 word ⊂_ txt 次は「大きいクラスほど上界は少ない」(反変)です。 !let goal := `A_ ⊂_ B_ ⟹ \{ cls x | ∀ y \, (y ∈_ B_ ⟹ y |..p^ x) \} ⊂_ \{ cls x | ∀ y \, (y ∈_ A_ ⟹ y |..p^ x) \}` thm goal -| O prf goal p-| O; txt 次は「もとのクラスは、その上界たちの下界に含まれる」です。上の反変と対で、ガロア接続の入口になります。 !let goal := `A_ ⊂_ \{ cls x | ∀ y \, (y ∈_ \{ cls z | ∀ u \, (u ∈_ A_ ⟹ u |..p^ z) \} ⟹ x |..p^ y) \}` thm goal -| O prf goal p-| O; br txt 写像についても書けます。 word ∩_ txt 次は「`.f` の不動点かつ `.g` の不動点なら、続けて施しても動かない」です。 !let goal := `\{ cls x | |.f x = x \} ∩_ \{ cls x | |.g x = x \} ⊂_ \{ cls x | |.f (|.g x) = x \}` thm goal -| O prf goal p-| O;
保存にはMatheliaへのログインが要ります。