preimage_inter_cod

Mathlib.Data.Rel

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

English

image (R ○ S) s = image S (image R s).

Русский

Образ композиции R ○ S от s равен образу S от образа R от s.

LaTeX

$$$\\forall (R : SetRel \\alpha \\beta) (S : SetRel \\beta \\gamma) (s : Set \\alpha),\\\\ image\\,(R \\circ S)\\,s = image\\,S\\,(image\\,R\\,s)$$$

Lean4

@[simp]
theorem preimage_inter_cod : preimage R (t ∩ R.cod) = preimage R t := by aesop

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

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

Разделы

Аффилиация

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