preimage_id_eq

Mathlib.Data.Set.Image

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

English

The preimage of the identity function is the identity on sets: preimage id = id.

Русский

Обратное образ тождественной функции равно тождественной функции.

LaTeX

$$$\operatorname{preimage}(\mathrm{id}) = \mathrm{id}.$$$

Lean4

@[simp]
theorem preimage_id_eq : preimage (id : α → α) = id :=
  rfl

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

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

Разделы

Аффилиация

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