.. _discrete_mathematics:

이산수학
========

*이산수학*\ 은 유한 집합, 객체, 구조에 대한 연구입니다. 유한 집합의 원소를 셀 수 있으며, 그 원소들에 대한 유한합이나 유한곱을 계산할 수 있고, 최댓값과 최솟값을 계산할 수 있는 등의 작업을 할 수 있습니다. 또한 특정 생성 함수를 유한 번 적용하여 생성되는 객체를 연구할 수 있고, 구조적 재귀로 함수를 정의할 수 있으며, 구조적 귀납법으로 정리를 증명할 수 있습니다. 이 장에서는 이러한 작업을 지원하는 Mathlib의 부분들을 설명합니다.

.. include:: C06_Discrete_Mathematics/S01_Finsets_and_Fintypes.inc
.. include:: C06_Discrete_Mathematics/S02_Counting_Arguments.inc
.. include:: C06_Discrete_Mathematics/S03_Inductive_Structures.inc