preimage_image

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Function.Injective.preimage_image

English

For an injective map, the preimage of the image equals the original set.

Русский

Для инъективного отображения прообраз образа равен исходному множеству.

LaTeX

$$$f^{ -1}(f(s)) = s$ (при $f$ инъективном).$$

Lean4

theorem preimage_image (hf : Injective f) (s : Set α) : f ⁻¹' (f '' s) = s :=
  preimage_image_eq s hf

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

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

Разделы

Аффилиация

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