preimage_univ_right

Mathlib.Data.Rel

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

English

For any relation R, the preimage of the universal set is the domain: preimage R univ = dom.

Русский

Для любого отношения R предобраз универсума равен области определения.

LaTeX

$$$\\forall (R : SetRel \\alpha \\beta), \\ preimage\\,R\\,\\mathsf{univ} = R.dom$$$

Lean4

@[simp]
theorem preimage_univ_right : preimage R .univ = R.dom := by aesop

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

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

Разделы

Аффилиация

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