invOn_id

Mathlib.Data.Set.Function

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

English

The identity map is its own inverse on any set.

Русский

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

LaTeX

$$$$\\forall s:\\, \\operatorname{InvOn}(\\mathrm{id}, \\mathrm{id}, s, s).$$$$

Lean4

theorem _root_.Set.invOn_id (s : Set α) : InvOn id id s s :=
  ⟨s.leftInvOn_id, s.rightInvOn_id⟩

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

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

Разделы

Аффилиация

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