Mathlib の命名規則¶
Mathlib の名前には強い規則性があります． 命名規則を知っていると，補題を推測したり，検索結果を読むのが楽になります．
基本方針は次の通りです．
- 定理名や証明項は
snake_case:add_comm,mul_assoc,not_le_of_gt - 型，命題，
structure，クラスはUpperCamelCase:Finset,MonoidHom,LinearOrder - 通常のデータや関数は
lowerCamelCase - 名前空間はドットで表す:
Nat.succ_ne_zero,Set.mem_inter_iff - 写像が構造を保つ補題は
map_add,map_mul,map_zeroのような名前になりやすい
ただし，古い名前や歴史的事情による例外もあります． 命名規則は検索の手がかりであって，完全な規格ではありません．
#check Nat.succ_ne_zero
#check Set.mem_inter_iff
#check Set.mem_union
#check add_comm
#check mul_assoc
#check map_add
記号に対応する語もある程度決まっています．
たとえば，∈ は mem，∩ は inter，∪ は union，≤ は le，< は lt，↔ は iff です．
したがって，集合の所属条件を探すときには mem_inter や mem_union のような名前を予想できます．
また，定理名では結論が先に来ることがよくあります．
たとえば not_le_of_gt は「> から ¬ ≤ が従う」と読みます．
この名前は，結論 not_le と仮定 of_gt に分けて読むと分かりやすくなります．
命名規則は公式の Mathlib naming conventions に整理されています． 新しい補題名を探すときは，記号を英語名に直し，名前空間と結論の形から推測するのが有効です．
演習¶
命名規則を使って，次の補題名を予想し，#check で確認してください．