3段階で考えよう
- 入れてよい値と、出てくる値の範囲を決めます。
- 関数は入力ごとに出力をちょうど一つ決めます。違う入力が同じ出力になっても構いません。
- Leanのα → βは、αの入力からβの出力への関数。fをxに適用するときはf xと書きます。
小さな例で確かめる
xをx × xへ送る規則は、2も−2も4に送ります。それでも関数です。
順番 7 / 64
高校
関数
関数は、入れてよい値のそれぞれに出力を一つ決めます。
まず、身近な例で
入力を二乗する機械なら、2を入れても−2を入れても4。同じ答えになる入力があっても関数です。一つの入力に、違う二つの答えを出すのはだめです。
ちいさな確認：考えてみよう
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
二乗する機械がその例です。同じ入力に違う二つの答えを出すのはだめですが、違う入力が同じ答えになっても構いません。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
はい、それぞれの入力の答えは一つ。 二乗する機械がその例です。同じ入力に違う二つの答えを出すのはだめですが、違う入力が同じ答えになっても構いません。
Leanでの使用例・原文の抜粋
FLT · aa2d8b3 · Def_FLTPrelim_Modularity.lean
def qCoeff (f : ℍ → ℂ) (n : ℕ) : ℂ :=(qExpansion 1 f).coeff n