image_inv

Mathlib.Data.Rel

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

English

The image under the inverse relation equals the preimage under the forward relation: R.inv.image t = preimage R t.

Русский

Изображение по обратному отношению равно предобразованию по прямому отношению: R.inv.image t = preimage R t.

LaTeX

$$R.inv.image\,t = preimage\,R\,t$$

Lean4

@[simp]
theorem image_inv : R.inv.image t = preimage R t :=
  rfl

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

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

Разделы

Аффилиация

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