bijOn_id

Mathlib.Data.Set.Function

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

English

The identity map on any set is BijOn.

Русский

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

LaTeX

$$$\\text{BijOn}(\\mathrm{id},S,S)$$$

Lean4

theorem bijOn_id (s : Set α) : BijOn id s s :=
  ⟨s.mapsTo_id, s.injOn_id, s.surjOn_id⟩

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

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

Разделы

Аффилиация

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