preimage_id

Mathlib.Data.Set.Image

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

English

For any set s, preimage of id on s is s: id^{-1} s = s.

Русский

Для любого множества s предобраз id на s равен s.

LaTeX

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

Lean4

@[mfld_simps]
theorem preimage_id {s : Set α} : id ⁻¹' s = s :=
  rfl

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

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

Разделы

Аффилиация

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