跳到正文
The Lumenary
六至八年级Ages 12–15 45 分钟

Functions

Rules that give exactly one output for every input — drawn as arrows, built from ordered pairs, and sorted into injective, surjective and bijective.

已形式化验证 · 6 Lean已通过计算测试 · 1 PythonAI 起草 · 等待人工审校已经数学审校: 等待人工审校

你的向导: Chloe, Margaret, Gideon

本页尚未翻译成简体中文,因此以English显示。

帮助翻译 →
引入H

One input, one output

Every student in a school has exactly one birth month. A vending machine gives exactly one snack for each button that works. A thermometer shows exactly one temperature at each moment.

Each of these is a rule that takes something in and gives exactly one thing out. Rules like this are everywhere: in science, in economics, in computer programs, and in every branch of mathematics. They are called functions.

定义H

What a function is

定义— function

A function ff from a set AA to a set BB, written f:A→Bf : A \to B, assigns to every element a∈Aa \in A exactly one element f(a)∈Bf(a) \in B.

  • AA is the domain — the allowed inputs.
  • BB is the codomain — where the outputs are allowed to live.
  • The image f(A)={ f(a)∣a∈A }f(A) = \{\, f(a) \mid a \in A \,\} is the set of outputs that actually occur. It is a subset of the codomain, but it need not be all of it.

Two conditions hide in the definition, and both matter:

  1. Every input has an output — nothing in AA is left out.
  2. Each input has exactly one output — no input is sent to two places.
探索

Explore: draw your own function

In an arrow diagram, each element of AA sends an arrow to its output in BB. Draw arrows below and watch the explorer check the two conditions — and more.

画一个函数

先点击 A 中的一个元素,再点击 B 中的一个元素,就能画出一个箭头。再次点击同一对即可删除。

A · 定义域B · 陪域123abc

点击 A 中的一个元素,开始画箭头。

  • 它是从 A 到 B 的函数吗?是:A 中每个元素恰好有一个箭头。
  • 单射(一对一)?没有两个箭头落在同一个元素上。
  • 满射(映上)?B 中每个元素都有箭头指向。
  • 双射?完美的配对:你可以把每个箭头都反过来。
例题讲解H

Examples and non-examples

例— Functions

  • f:Z→Zf : \Z \to \Z, f(n)=2n+1f(n) = 2n + 1. Every integer has exactly one output; the image is the set of odd integers.
  • s:Z→Zs : \Z \to \Z, s(n)=n2s(n) = n^2. The image is {0,1,4,9,… }\{0, 1, 4, 9, \dots\}, which is smaller than the codomain Z\Z.
  • The rule sending each student to their birth month is a function from the set of students to the set of twelve months.

例— Not functions

  • "Send each person to their sibling" is not a function from people to people: some people have several siblings, and some have none.
  • "Send each integer nn to a number whose square is nn" fails twice: 44 has two square roots, 22 and −2-2, and −1-1 has none in Z\Z.
定义H

Injective, surjective, bijective

定义— injective (one-to-one)

f:A→Bf : A \to B is injective if different inputs always give different outputs: whenever f(x)=f(y)f(x) = f(y), we have x=yx = y.

定义— surjective (onto)

f:A→Bf : A \to B is surjective if every element of the codomain is an output: for every b∈Bb \in B there is some a∈Aa \in A with f(a)=bf(a) = b.

定义— bijective

ff is bijective if it is both injective and surjective. A bijection pairs the elements of AA and BB perfectly, so it can be reversed.

Surjectivity depends on the codomain you choose. s(n)=n2s(n) = n^2 is not surjective as a function Z→Z\Z \to \Z, but it is surjective onto its image {0,1,4,9,… }\{0, 1, 4, 9, \dots\}.

证明H

Proving the properties

定理— injective

f:Z→Zf : \Z \to \Z, f(n)=2n+1f(n) = 2n + 1, is injective.

证明

Suppose f(x)=f(y)f(x) = f(y), that is, 2x+1=2y+12x + 1 = 2y + 1. Subtracting 11 gives 2x=2y2x = 2y, and dividing by 22 gives x=yx = y.

∎

定理— not injective

s:Z→Zs : \Z \to \Z, s(n)=n2s(n) = n^2, is not injective.

证明

One counterexample is enough: s(1)=1=s(−1)s(1) = 1 = s(-1), but 1≠−11 \neq -1.

∎

定理— not surjective

d:Z→Zd : \Z \to \Z, d(n)=2nd(n) = 2n, is not surjective.

证明

Every output 2n2n is even, so the odd number 11 is never an output.

∎

形式化数学F

Functions in Lean

Lean's core library defines Function.Injective f to mean ∀ a b, f a = f b → a = b — exactly our definition. Here are the proofs above, machine-checked:

injective_two_mul_add_oneLean 4在此由基本事实证明已形式化验证
/-- `n ↦ 2n + 1` is injective: if `2a + 1 = 2b + 1`, subtract 1 and divide by 2. -/
theorem injective_two_mul_add_one : Injective (fun n : Int => 2 * n + 1) := by
  intro a b h
  -- `h : 2 * a + 1 = 2 * b + 1`
  have h1 : 2 * a = 2 * b := (Int.add_left_inj 1).mp h      -- subtract 1
  exact Int.eq_of_mul_eq_mul_left (by decide) h1           -- divide by 2 (and 2 ≠ 0)
使用的公理: propextformal/Lumenary/Functions.lean在 Lean 网页编辑器中试一试
not_injective_squareLean 4在此由基本事实证明已形式化验证
/-- `n ↦ n²` is **not** injective on the integers: `1² = (-1)²` but `1 ≠ -1`. -/
theorem not_injective_square : ¬ Injective (fun n : Int => n * n) := by
  intro h
  have h1 : (1 : Int) = -1 := h (by decide)   -- the hypothesis needed is `1 * 1 = -1 * -1`
  exact absurd h1 (by decide)
使用的公理: 未使用公理formal/Lumenary/Functions.lean在 Lean 网页编辑器中试一试
not_surjective_two_mulLean 4在此由基本事实证明已形式化验证
/-- `n ↦ 2n` is **not** surjective on the integers: nothing is sent to `1`, because there is
no integer half (`Lumenary.Integers.no_int_half`). -/
theorem not_surjective_two_mul : ¬ Surjective (fun n : Int => 2 * n) := by
  intro h
  obtain ⟨x, hx⟩ := h 1          -- `hx : 2 * x = 1`
  exact Lumenary.Integers.no_int_half ⟨x, hx⟩
使用的公理: propextformal/Lumenary/Functions.lean在 Lean 网页编辑器中试一试
bijective_negLean 4在此由基本事实证明已形式化验证
/-- Negation `n ↦ -n` is a bijection of the integers (it is its own inverse). -/
theorem bijective_neg : Bijective (fun n : Int => -n) := by
  constructor
  · -- Injective: from `-a = -b`, negate both sides.
    intro a b h
    exact Int.neg_inj.mp h
  · -- Surjective: `-(-y) = y`.
    intro y
    exact ⟨-y, Int.neg_neg y⟩
使用的公理: 未使用公理formal/Lumenary/Functions.lean在 Lean 网页编辑器中试一试
与集合论的联系H

A function is a set of ordered pairs

In set theory, a function is not a "machine" or a "formula" — it is a set. The graph of f:A→Bf : A \to B is

Γf={ (a,f(a))∣a∈A }⊆A×B.\Gamma_f = \{\, (a, f(a)) \mid a \in A \,\} \subseteq A \times B.

A subset R⊆A×BR \subseteq A \times B is the graph of a function exactly when each a∈Aa \in A appears as the first coordinate of exactly one pair in RR. That is the definition of a function used throughout modern mathematics: it is precise, and it doesn't care whether the rule has a formula.

graph_functionalLean 4在此由基本事实证明已形式化验证
/-- A graph is **functional**: each input `a` is paired with `f a`, and with nothing else. -/
theorem graph_functional (f : α → β) (a : α) :
    graph f (a, f a) ∧ ∀ b, graph f (a, b) → b = f a := by
  constructor
  · -- `graph f (a, f a)` says `f a = f a`.
    rfl
  · intro b h
    -- `h : f a = b`
    exact Eq.symm h
使用的公理: 未使用公理formal/Lumenary/Functions.lean在 Lean 网页编辑器中试一试

注

Lean is built on type theory rather than set theory, so its functions are a basic notion rather than sets of pairs. The graph above shows that the two viewpoints agree on what a function does. They are different foundations, not interchangeable ones.

计算C

How many functions are there?

If ∣A∣=m|A| = m and ∣B∣=n|B| = n, each of the mm inputs independently chooses one of nn outputs, so there are nmn^m functions A→BA \to B. Injective functions are rarer: the first input has nn choices, the next n−1n - 1, and so on, giving n(n−1)⋯(n−m+1)n(n-1)\cdots(n-m+1).

Counting functions, injections and surjectionsPython有限穷举检验精确计算已通过计算测试
"""Counting functions between small finite sets.

A function f: A -> B picks one output in B for every input in A. If A has m
elements and B has n, we can list every function as a tuple
(f(a_1), ..., f(a_m)) using ``itertools.product``. We count how many are
injective (one-to-one), surjective (onto) and bijective, and compare the
counts with the standard formulas:

    all functions   n^m
    injective       n (n-1) ... (n-m+1)          (the falling factorial)
    surjective      sum_k (-1)^k C(n,k) (n-k)^m  (inclusion-exclusion)
    bijective       m! when m = n, otherwise 0

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from itertools import product
from math import comb, factorial
import textwrap

def all_functions(domain, codomain):
    """Return every function domain -> codomain as a dict {input: output}.

    There are len(codomain) ** len(domain) of them; for an empty domain there is
    exactly one (the empty function).
    """
    domain, codomain = list(domain), list(codomain)
    return [dict(zip(domain, outputs)) for outputs in product(codomain, repeat=len(domain))]

def is_injective(f):
    """True when different inputs always give different outputs."""
    outputs = list(f.values())
    return len(set(outputs)) == len(outputs)

def is_surjective(f, codomain):
    """True when every element of the codomain is an output of f."""
    return set(f.values()) == set(codomain)

def is_bijective(f, codomain):
    """True when f is both injective and surjective."""
    return is_injective(f) and is_surjective(f, codomain)

def count_by_enumeration(m, n):
    """Enumerate all functions {0..m-1} -> {0..n-1}; return a dict of counts."""
    domain, codomain = range(m), range(n)
    functions = all_functions(domain, codomain)
    return {
        "all": len(functions),
        "injective": sum(is_injective(f) for f in functions),
        "surjective": sum(is_surjective(f, codomain) for f in functions),
        "bijective": sum(is_bijective(f, codomain) for f in functions),
    }

def falling_factorial(n, k):
    """n (n-1) ... (n-k+1), the number of ways to choose k distinct items in order.

    Equals 1 when k = 0 and 0 when k > n.
    """
    if n < 0 or k < 0:
        raise ValueError("n and k must be non-negative")
    result = 1
    for i in range(k):
        result *= n - i
    return result

def surjection_formula(m, n):
    """Number of surjections from an m-set onto an n-set, by inclusion-exclusion.

    sum over k = 0..n of (-1)^k C(n, k) (n - k)^m, using Python's 0 ** 0 == 1.
    """
    if m < 0 or n < 0:
        raise ValueError("m and n must be non-negative")
    return sum((-1) ** k * comb(n, k) * (n - k) ** m for k in range(n + 1))

def formula_counts(m, n):
    """The counts predicted by the formulas, in the same shape as :func:`count_by_enumeration`."""
    return {
        "all": n ** m,
        "injective": falling_factorial(n, m),
        "surjective": surjection_formula(m, n),
        "bijective": factorial(m) if m == n else 0,
    }

def main():
    sizes = [(m, n) for m in range(1, 5) for n in range(1, 5)]
    print("Every function A -> B, |A| = m and |B| = n, listed with itertools.product.")
    print("Each cell shows: counted by enumeration / predicted by the formula.")
    print()
    print(f"{'m':>2} {'n':>2} | {'all  (n^m)':>11} | {'injective':>9} | {'surjective':>10} | {'bijective':>9}")
    print("-" * 57)
    agree = 0
    listed = 0
    for m, n in sizes:
        counted, predicted = count_by_enumeration(m, n), formula_counts(m, n)
        listed += counted["all"]
        agree += counted == predicted
        cells = [f"{counted[k]}/{predicted[k]}" for k in ("all", "injective", "surjective", "bijective")]
        print(f"{m:>2} {n:>2} | {cells[0]:>11} | {cells[1]:>9} | {cells[2]:>10} | {cells[3]:>9}")
    print()
    print(f"Listed {listed} functions; enumeration and formulas agree for {agree} of {len(sizes)} size pairs.")
    empty = [count_by_enumeration(0, n)["all"] for n in range(5)]
    print("Edge cases: from the empty set to a set of size 0, 1, 2, 3, 4 there are")
    print(f"{empty} functions (exactly one: the empty function);")
    print(f"from a 2-element set to the empty set there are {count_by_enumeration(2, 0)['all']}.")
    print()
    print(textwrap.fill(
        f"Epistemic status: exhaustive enumeration proves these counts for the "
        f"{len(sizes)} size pairs shown, and the formulas match them exactly. That the "
        "formulas hold for every m and n is a theorem proved by counting "
        "arguments; this table is consistent with it but does not prove it.",
        width=78,
    ))

if __name__ == "__main__":
    main()
完全在你的浏览器中、在一个隔离的工作线程里运行。不会向服务器发送任何内容。
练习

Exercises

1. Functions

热身人类思维

Let A={1,2,3}A = \{1, 2, 3\} and B={a,b}B = \{a, b\}. Which of these rules is a function from AA to BB?

选择一项

2. Functions

核心人类思维

How many functions are there from a set with 33 elements to a set with 22 elements?

3. Functions

核心人类思维

How many injective functions are there from a 2-element set to a 4-element set?

4. Functions

核心人类思维

Which of these functions Z→Z\Z \to \Z are surjective? (Choose all that apply.)

选择所有符合的选项

5. Functions

挑战人类思维

A school has 400 students. Why must at least two of them share a birthday (day and month)?

选择一项

6. Functions

挑战计算

A finite function can be stored as a Python dictionary, e.g. {1: 'a', 2: 'b', 3: 'a'}. Write is_injective(f) returning True exactly when no two keys have the same value.

完全在你的浏览器中、在一个隔离的工作线程里运行。不会向服务器发送任何内容。
常见误解H

Common misconceptions

误解

"A function must have a formula." The birth-month function has no formula. A function is any rule — or any set of pairs — giving exactly one output per input.

误解

"The codomain is the same as the image." The codomain is where outputs are allowed to be; the image is where they actually are. Whether ff is surjective is precisely the question of whether they coincide.

误解

"Exactly one output means exactly one input." A function may send many inputs to the same output (n2n^2 does). That is allowed; it just means the function is not injective.

误解

"f(a+b)=f(a)+f(b)f(a + b) = f(a) + f(b) for every function." True for f(n)=3nf(n) = 3n, false for f(n)=n2f(n) = n^2 or f(n)=n+1f(n) = n + 1. Functions that respect addition are special — they are called homomorphisms.

探奇小径

Wonder Trail

与范畴论的联系H

Functions as arrows

Arrow diagrams are more than a teaching picture. In much of modern mathematics, structures are studied through the arrows between them — functions between sets, structure-preserving maps between groups, continuous maps between spaces. The crucial operation on arrows is following one arrow and then another: composition, the subject of the next lesson.

历史与全球视野

History and global context

  • Tables recording how one quantity depends on another are ancient. In India, Āryabhaṭa's Āryabhaṭīya (499 CE) includes a table for computing sines, and astronomers in many cultures tabulated the positions of the Sun, Moon and planets over time.
  • In the 14th century, Nicole Oresme drew diagrams showing how a quality varies with another quantity — an early ancestor of the graph.
  • Gottfried Wilhelm Leibniz used the word function in the late 17th century; Leonhard Euler introduced the notation f(x)f(x) in 1734. In 1837 Peter Gustav Lejeune Dirichlet described functions as arbitrary correspondences, not necessarily given by formulas.
  • In the early 20th century, mathematicians began defining functions as sets of ordered pairs, the definition used in this lesson.
延伸阅读

Further reading

  • Richard Hammack, Book of Proof (3rd edition, 2018) — free to read; chapters on functions and on proof techniques.
  • Daniel J. Velleman, How to Prove It (2nd edition, 2006).