Leanのvariable
variable (<変数の名前> : <変数の型名>)
https://aconite-ac.github.io/theorem_proving_in_lean4_ja/dependent_type_theory.html#variables-and-sections-変数とセクション
宣言された箇所から、1ファイルの最後まで有効
ただしsectionでスコープを作れる