rightInvOn_id

Mathlib.Data.Set.Function

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

English

The identity function is a right inverse of itself on any set.

Русский

Идентичная функция является правым обратным самой себе на любом множестве.

LaTeX

$$$$ \\text{_root_.Set.rightInvOn_id } s = \\text{RightInvOn } id id s. $$$$

Lean4

theorem _root_.Set.rightInvOn_id (s : Set α) : RightInvOn id id s := fun _ _ ↦ rfl

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

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

Разделы

Аффилиация

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