2021-01-01から1年間の記事一覧

今日の証明

現代数学概説Ⅰ 1章 $2 例題3 以下を示せ。 G1 ⊆ G1', G2 ⊆ G2'ならばG2・G1 ⊆ G2'・G1' Gx・GyはGxとGyの合成。 ------------------------------------------------------------------------- 対応Γ1を (G1, M1, M2) : 表すと集合M1から M2への対応のグラ…

長めの朝練ー六甲山

6/17(木) 代休を取って長めの朝練に出かけた。 予定では、佐保⇒余野⇒池田⇒猪名川⇒安威川遡上、時間にして3時間ちょいで帰宅だったが。。あまりにも天候が良くて池田で進路変更、西に向けて進路を取った。 目的地は六甲山。。経路は逆瀬川ルート。 選択理由…

草津ナイトレース・#2

草津ナイトレース・#2へ行ってきた。 結果は、無事完走(同一周回!)。 今回はクラスを一つ上げて、目標を”ゴールスプリントにからむ” で挑んだが、途中でちぎれてしまった。 今回は、車をレンタルした。 当初の予定では京都河原町駅から自走を予定していた…

草津ナイトレース・#1

草津ナイトレース#1へ自走で出走してきた。 結果は。。 スタートラインに並んだ時の走行距離104.3km。。ゴール時は112km。 ほんの少し、ツールド沖縄100kmの部で完走した気分になれた。 -- 詳細は後日 -- 行き経路ー琵琶湖大橋を通った。 競技時の軌跡 帰路…

今日の証明

現代数学概説Ⅰ 1章 $2 例題2 以下を示せ。 1) Γ(x) ∍y ⇔ Γ.exp-1(y)∍x. 2) A'⊆A⊆M とする時 Γ(A')⊆Γ(A). 3) B'⊆B⊆N とする時 Γ.exp-1(B')⊆Γ.exp-1(B). 4) A⊆DomΓ とする時 A⊆Γ.exp-1 (Γ(A)). 5) B⊆ImΓ とする時 B⊆Γ(Γ.exp-1(A)). 注) .exp-1はマイナス1乗を…

烏丸半島サイクリング 雨に降られた。

昨日の土曜日(5/22)に烏丸半島までサイクリングしてきた。 注)琵琶湖大橋近くに有る。 行きは、宇治→瀬田川経由して烏丸半島まで。 帰路は、京都四条河原を経由して帰宅。 四条河原町手前で雨が降り出して来た。河原町駅前で雨宿り中にスマホでレーダ画を見…

大山山系・縦走 船上山⇒矢筈⇒大休峠⇒川床

5/3(月)憲法記念日 船上山⇒矢筈⇒大休峠⇒川床⇒船上山経由で縦走してきた。 非常事態宣言中でおとなしくしている予定であったが、自宅に帰る用事が出来た。 そのついでに、山を歩いた。 大休峠でカメラの電池が切れた。 従って、川床までの画像は無い。 川床か…

今日の証明

現代数学概説Ⅰ 1章 $1 例題9 M⊆M', N⊆N⇒MxN⊆M'xN'であって、 (MxN).c(Ωmn) = (M.c(Ωm)xN') ∪ (M'xN.(Ω=N')). 注) AxBはA,Bの直積を表す。A.c(Ωxx)はAの補集合で(Ω)内は母集合を表す。 Ωmn=M'xN', Ωm=M', Ωn=N'. ---------------------------------------- a)…

今日の証明

現代数学概説Ⅰ 1章 $1 例題4 以下b)を示せ。 b) M ⊆ N <-> M = M ∩ N <-> N = M ∪ N. ------------------------------------------------------------------ Theorem math_1_1_exp_4b_ab: forall (M N:Ensemble M), M ⊆ N <-> M = M ∩ N.Proof. intros M N. …

今日の証明

現代数学概説Ⅰ 1章 $1 例題4 以下a)b)c)を示せ。 a) M ∪ (M ∩ N)=M, M ∩ (M ∪ N) = M. b) M ⊆ N <-> M = M ∩ N <-> N = M ∪ N. c) M ⊆ M' <-> M ∪ N ⊆ M' ∪ N, M ∩ N ⊆ M' ∩ N. ----- coq 証明 a) Theorem math_1_1_exp_4a1: forall (M N:Ensemble M), M ∪ (…

今日の証明

現代数学概説Ⅰ 1章 $1 例題6 M-N = ∅ ⇔ N⊃Mを示せ。 ------------------ 下記a),b)を示せばよい。 a) M-N = ∅ ⇒ N ⊃ M. b) N ⊃ M ⇒ M-N = ∅. --- a) N ⊃ M = {x| M∍x ⇒ N ∍ x}. ...(1)より ゆえにNはMの要素をすべて含む。 従って、M-N=∅ □ b) M-N = ∅なので…

六甲山 桜サイクリング

4/21(水) 代休を取って 六甲山へ桜を見に出かけた。 経路は、茨木⇒宝塚⇒有馬⇒裏六甲⇒一軒家茶屋⇒神戸駅⇒淀川⇒帰宅 有馬⇒裏六甲経由にしたのは、坂が多少は緩いため。 ⇒激坂はチェーンが早く伸びるのだ。。「てこの原理」に由来する(機械工学の学士様が言う…

六甲山 桜サイクリング

4/21(水) 代休を取って 六甲山へ桜を見に出かけた。 経路は、茨木⇒宝塚⇒有馬⇒裏六甲⇒一軒家茶屋⇒淀川⇒帰宅 -- 内容は後日 -- 裏六甲の桜 一軒家茶屋 六甲稜線の桜 淀川

今日の証明

現代数学概説Ⅰ(彌永昌吉、小平邦彦)の例題1を解いてみた。 ---------------- x(∊R)を超えない最大整数を[x](gaussの記号)で表す時、集合{x : x∊R,[x]=n} (nはある定まった整数)は区間[n,n+1)に等しい。 --- * 俺注) {x : x∊R, a ≦x<b}を[a,b)と略記する。…

北摂⇒嵐山⇒瀬田川⇒背割り堤サイクリング

4/1(木)代休を取って桜サイクリングに出かけた。 経路は北摂山中⇒嵐山⇒鴨川⇒瀬田川⇒宇治⇒淀川。 -- 詳細は後日 -- GPS軌跡 北摂山中の桜 嵐山の桜 三条大橋の桜 瀬田川の桜 宇治橋 背割り堤の桜 茨木の桜

今日の証明

TAPL演習の2.2.6を解いてみた。 【問題】 集合S上の関係Rを与え、関係R’を以下の様に定義する。 R' = R ∪ { (s,s) | S ∍s } R'が反射的閉包であることを示せ。 --------------------------------------------- 反射的閉包は定義2.2.1及び2.2.5より下記の条件…

3.11メモリアルCXに出走してきた。

富田林でメモリアルCXがあり出走してきました。 今季で10回目、今年で最後にするそうです。 レースの方は、いつもの着順で変わり映えなしとな感じで終わりました。 出走したレースは60分耐久(30分x2)とスプリント。 合計3レース走りました。 1レース…

今日の証明

ここのところ、SOFTWARE FOUNDATIONSに取り組んでいます。 これは、coqを使用して「高信頼ソフトウェアに関する広範囲の数学的基礎を学べる。」とのことです。 本日完了したのは、第一巻のinduction:帰納法による証明まで、練習問題が用意されており下記に示…

元旦の朝練

あけましておめでとうございます。 令和3年元旦 元旦の高槻方面