coercion と subtype

Mathlib では，自然な埋め込みは coercion として登録されています． たとえば自然数を実数として使うとき，((3 : Nat) : ℝ) のように型を変換します． coercion は便利ですが，エラーメッセージを読むときには「Lean がどの型からどの型へ自動変換したのか」を意識する必要があります．

example : ((3 : Nat) : ℝ) = 3 := by
  norm_num

Subtype は，条件を満たす要素を集めた型です． {n : Nat // 0 < n} は，正の自然数とその証明を組にした型です． 値を元の型に戻すときは coercion が働きます． x.property は，x が subtype の条件を満たすことの証明です．

example (x : {n : Nat // 0 < n}) : 0 < (x : Nat) := by
  exact x.property

ここまでが，Mathlib の定義や定理を読むための一般的な見方です． 以下では，数学で頻繁に使う具体的な型を順に見ます．