import Mathlib と open scoped¶
このプロジェクトでは各章の冒頭で import Mathlib を使っています．これは Mathlib 全体を読み込みます．
実際の開発では，ビルド時間を抑えるために必要なファイルだけを import することもあります．
たとえば import Mathlib.Data.Real.Basic や import Mathlib.Topology.Basic のように，必要な分野のファイルだけを import する書き方です．
import Mathlib は「Mathlib に含まれる主要な定義・定理・tactic をまとめて使えるようにする」指定であり，Lean の言語機能そのものとは区別します．
一部の notation は，スコープを開かないと使えません．
有限和 ∑ には BigOperators，拡張非負実数の ∞ には ENNReal のスコープを使います．
open scoped は名前空間の中の定義名を短くするというより，特定の notation やスコープ付き notation を有効にするために使います．
Mathlib では，定義そのものと notation が分かれていることがよくあります．
たとえば Real という型には ℝ という notation があり，NNReal には ℝ≥0，ENNReal には ℝ≥0∞ という notation があります．
また ∑ i ∈ s, f i は有限和を表す notation で，背後には Finset.sum があります．
証明中で notation の意味が分からなくなったら，#check で型を確認し，必要なら対応する定義名を探します．
#check は，Mathlib の名前がどのような型をもつかを確認する基本コマンドです．
#synth は，指定した型クラスインスタンスを Lean が見つけられるかを確認します．
#check Finset
#check Set
#check Real
#check NNReal
#check EReal
#check ENNReal
#check ℝ
#check ℝ≥0
#check ℝ≥0∞
#check (∞ : ℝ≥0∞)
#synth Field ℝ
#synth LinearOrder ℝ
#synth TopologicalSpace ℝ
#synth Add ENNReal
#synth CompleteLinearOrder ENNReal
演習¶
#synth で，実数が体・線形順序・狭義順序環の構造を持つことを確認してください．