mapsTo_id

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.mapsTo_id

English

The identity map maps any set to itself.

Русский

Идентичное отображение отображает любое множество в себя.

LaTeX

$$$ MapsTo\\ id\\ s\\ s $$$

Lean4

theorem mapsTo_id (s : Set α) : MapsTo id s s := fun _ => id

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru