.. _sets_and_functions:

집합과 함수
===========

집합, 관계, 함수의 어휘는 수학의 모든 분야에서 구성을 수행하기 위한 통일된 언어를 제공합니다. 함수와 관계는 집합을 통해 정의될 수 있으므로, 공리적 집합론은 수학의 기초로 사용될 수 있습니다.

대신 Lean의 기초는 *타입*\ 이라는 원시 개념에 기반하며, 타입 간 함수를 정의하는 방법을 포함합니다. Lean의 모든 표현식은 타입을 가집니다. 자연수, 실수, 실수에서 실수로의 함수, 군, 벡터 공간 등이 있습니다. 어떤 표현식은 그 자체로 타입\ *입니다*, 즉 그 타입은 ``Type``\ 입니다. Lean과 Mathlib는 새로운 타입을 정의하는 방법과 해당 타입의 객체를 정의하는 방법을 제공합니다.

개념적으로, 타입을 단순히 객체의 집합으로 생각할 수 있습니다. 모든 객체가 타입을 가지도록 요구하는 것에는 몇 가지 이점이 있습니다. 예를 들어, 이는 ``+``\ 와 같은 표기법을 중복 정의할 수 있게 하며, Lean이 객체의 타입으로부터 많은 정보를 추론할 수 있기 때문에 입력을 덜 장황하게 만들기도 합니다. 또한 타입 시스템은 함수에 잘못된 개수의 인수를 적용하거나 잘못된 타입의 인수를 함수에 적용할 때 Lean이 오류를 표시할 수 있게 해줍니다.

Lean의 라이브러리는 기본적인 집합론적 개념들을 정의합니다. 집합론과 달리, Lean에서 집합은 항상 어떤 타입에 속한 대상들의 집합입니다. 예를 들어 자연수의 집합이나 실수에서 실수로 가는 함수들의 집합과 같은 것입니다. 타입과 집합의 구분에 익숙해지려면 다소 시간이 걸리지만, 이 장에서 그 핵심을 안내해 드리겠습니다.

.. include:: C04_Sets_and_Functions/S01_Sets.inc
.. include:: C04_Sets_and_Functions/S02_Functions.inc
.. include:: C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.inc