image_inter_dom

Mathlib.Data.Rel

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

English

image R (s ∩ dom(R)) = image R s.

Русский

Образ через R от пересечения s с dom(R) совпадает с образом s через R.

LaTeX

$$$\\forall (R : SetRel \\alpha \\beta) (s : Set \\alpha),\\\\ image\\,R\\,(s \\cap R.dom) = image\\,R\\,s$$$

Lean4

@[simp]
theorem image_inter_dom : image R (s ∩ R.dom) = image R s := by aesop

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

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

Разделы

Аффилиация

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