Step 7 / 64

High school

Functions

A function gives one output for each permitted input.

Start with a concrete example

A machine that squares its input sends 2 to 4 and −2 to 4. Different inputs may share an output. A single input must not give two different answers.

A small check: try the idea

Think with the concrete example above. You can try again.

Can a function send both 2 and −2 to 4?

Read the answer and reasoning

Yes; each input still has one output. The squaring machine does exactly this. A function forbids two different outputs for the same input, not one shared output for two inputs.

Build the idea in three steps

  1. Choose a set of allowed inputs and a set of outputs.
  2. A function assigns exactly one output to each input. Different inputs may share an output.
  3. Lean writes α → β for a function from inputs of type α to outputs of type β. Applying f to x is written f x.

A small example

A rule that sends x to x × x sends both 2 and −2 to 4. It is still a function.

Use in Lean · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_Modularity.lean

def qCoeff (f : ℍ → ℂ) (n : ℕ) : ℂ :=  (qExpansion 1 f).coeff n

How to read this Lean

The input f is itself a function. ℍ → ℂ says its input is a point of the upper half-plane and its output a complex number. The additional n selects a coefficient.

Where this idea is used

5. The suspicious parcel6. The scissors incident8. The secret duet9. Two doors to the concert10. A three-note audition11. Borrow a better passport12. The workshops agree13. Pip’s impossible quilt14. The shrinking reservation15. The concert of absolute silence16. The room with no room
I’m lost · Help

Mika’s help desk

Functions

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

A function gives one output for each permitted input.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

A rule that sends x to x × x sends both 2 and −2 to 4. It is still a function.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →