implicit指定

半形式証明スクリプト

\require{color}% \newcommand{\In}{\text{ in }}% \newcommand{\R}{{\bf R}}% \newcommand{\id}{ \mathrm{id}}% \newcommand{\For}{\mbox{For }}% \newcommand{\wh}[1]{\widehat{ #1 }}% \newcommand{\Imp}{\Rightarrow }% \newcommand{\Keyword}[1]{\textcolor{green}{#1} }% \newcommand{\For}{\Keyword{ \mbox{For } } }% \newcommand{\implicit}{\Keyword{ \mbox{ implicit } } }% \newcommand{\Define}{\Keyword{\mbox{Define } }}% \newcommand{\Let}{\Keyword{\text{Let } }}% \newcommand{\Where}{\Keyword{\text{Where} }}%

暗黙の前提を書くのに implicit でマークする。共変微分の接続形式を定義する例。

\For \implicit M \In {\bf Man}, E \In {\bf VectBdl}[M]\\ \Let r := rank(E)\\ \For \nabla \in CovDer(E) \\ \For U \In Open(M), e \in Frame(U, E) \\ \Define \gamma_U(\nabla, e) := e^\star (\nabla) - D_U^r \\ \Where\\ \quad D_U^r := CanDer(U, r) \text{ // canonical derivative}

implicit を増やすと：

\For \implicit M \In {\bf Man}, E \In {\bf VectBdl}[M]\\ \quad \nabla \in CovDer(E), U \In Open(M) \\ \Let r := rank(E)\\ \For e \in Frame(U, E) \\ \Define \gamma(e) := e^\star (\nabla) - D^r \\ \Where\\ \quad \For \implicit U \In Open(M) \\ \quad \Define D^r := CanDer(U, r) \text{ // canonical derivative}

\gamma の引数がフレームだけになる。