doc-src/TutorialI/Sets/sets.tex
changeset 10888 f321d21b9a6b
parent 10857 47b1f34ddd09
child 10978 5eebea8f359f
equal deleted inserted replaced
10887:7fb42b97413a 10888:f321d21b9a6b
   400 A\ \isasymand\ card\ B\ =\
   400 A\ \isasymand\ card\ B\ =\
   401 k\isacharbraceright\ =\ card\ A\ choose\ k%
   401 k\isacharbraceright\ =\ card\ A\ choose\ k%
   402 \rulename{n_subsets}
   402 \rulename{n_subsets}
   403 \end{isabelle}
   403 \end{isabelle}
   404 Writing $|A|$ as $n$, the last of these theorems says that the number of
   404 Writing $|A|$ as $n$, the last of these theorems says that the number of
   405 $k$-element subsets of~$A$ is $n \choose k$.
   405 $k$-element subsets of~$A$ is $\binom{n}{k}$.
   406 
   406 
   407 \begin{warn}
   407 \begin{warn}
   408 The term \isa{Finite\ A} is an abbreviation for
   408 The term \isa{Finite\ A} is an abbreviation for
   409 \isa{A\ \isasymin\ Finites}, where the constant \isa{Finites} denotes the
   409 \isa{A\ \isasymin\ Finites}, where the constant \isa{Finites} denotes the
   410 set of all finite sets of a given type.  There is no constant
   410 set of all finite sets of a given type.  There is no constant