leftInvOn_id

Mathlib.Data.Set.Function

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

English

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

Русский

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

LaTeX

$$$$ \\text{LeftInvOn } id id s. $$$$

Lean4

theorem _root_.Set.leftInvOn_id (s : Set α) : LeftInvOn id id s := fun _ _ ↦ rfl

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

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

Разделы

Аффилиация

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