Lines Matching refs:function
10 function is a set, and the inverse image of a function maps sets to sets.
446 \indexbold{updating a function}%
456 \isa{(f(x:=y))\ z} we are applying an updated function to an
467 The \bfindex{identity function} and function
489 A function may be \textbf{injective}, \textbf{surjective} or \textbf{bijective}:
502 of \isa{inj_on} lets us express that a function is injective over a
504 functions are total; in some cases, a function's natural domain is a subset
509 \textbf{inverse}\indexbold{inverse!of a function}
510 of a function. In
535 %The converses of these results fail. Unless a function is
556 function composition:
576 The \textbf{image}\indexbold{image!under a function}
577 of a set under a function is a most useful notion. It
612 \index{range!of a function}%
613 A function's \textbf{range} is the set of values that the function can
615 that function. There is no constant \isa{range}. Instead,
627 \textbf{Inverse image}\index{inverse image!of a function} is also useful.
703 analogously to image under a function:
875 termination~\cite{isabelle-function}. Most of the forms of induction found
887 \index{measure functions}\textbf{measure function}~\isa{f} into
894 complex recursive function definition or induction. The induction rule
912 a relation. Given a relation~\isa{r} and a function~\isa{f}, we express a
925 A measure function involves the natural numbers. The relation \isa{measure