仕事ではReactで開発を行っていますが、React Nativeを使った開発をしたことがなかったので調べてみました。 expo-cliをインストール。 Expo CLIでReact Nativeプロジェクトを作成します。 プロジェクトの作成が終わったらディレクトリに入って開発サーバーを起動してみます。 ここで起動されるサーバーは、プロジェクトの管理サーバーのようです。 サイドバーのRun in web browserを押してローカルで起動させてみます。 ブラウザが開いて下のフレーズが画面に出てくればうまくいっています。 Open up App.tsx to start working on your app! サーバーがうまく立ち上がっていることを確認出来たら、いつものフレーズを追加します。 ファイルを保存すると画面に表示されているテキストが変わっているはずです。 Open up App.tsx to start working on your app!Hello React Native! スマホアプリの開発が思ったより簡単に始められることがわかったので、テンションあがりますね！ 参考： ゼロから始める React Native + Expo 入門
Month: April 2022
Cantorの対角線論法
今回はLean4でCantorの定理（と同等の定理）を証明します。 Cantorの定理 集合Aに対し、集合Aからその冪集合への全射写像 [katex]f : A \to 2^A[/katex] は存在しない。 ※厳密なCantorの定理はCardinalを定義する必要がありますので、その話はまた別の機会に行いたいと思います。 Lean4でCantorの定理は以下でかけます。 これをLean4で解いてみます。 Cantorの定理を証明する場合、αのある部分集合を使って証明する手法がよく採用されます。 Cantorの補題 Aを集合Aとし、fを集合Aからその冪集合への写像 [katex]f : A \to 2^A[/katex] とする。このとき、Bを [katex]\{ a \in A | a \notin f(a) \}[/katex] とすると、 [katex]f(a)=B[/katex] なる [katex]a \in A[/katex] は存在しない。 この補題を絡めて、証明を途中まで埋めます。 Cantorの補題の証明は [katex]a \in A[/katex] と、[katex]a \notin A[/katex] についてどちらも矛盾となることで示します。 Lean4の証明でもその方針で証明してみます。Lean4で排中律を使いたい場合は by_cases を使います。 sorryの部分を埋めます。 D ∈ f D の場合…