preimage_id

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.preimage_id

English

For any s, the preimage of s under the identity relation equals s: preimage .id s = s.

Русский

Предобраз множества s под идентичным отношением равен самому s.

LaTeX

$$$\\forall (s : Set \\alpha), \\ preimage .id\\,s = s$$$

Lean4

@[simp]
theorem preimage_id : preimage .id s = s := by aesop

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

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

Разделы

Аффилиация

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