preimage_inv

Mathlib.Data.Rel

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

English

Again, the same relation between preimage under the inverse and image: R.inv.preimage s = image R s.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_inv : R.inv.preimage s = image R s :=
  rfl

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

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

Разделы

Аффилиация

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