image_comp — Mathlib

English

For any R, S, and s, the image under the composition R ○ S equals the image under S of the image under R: 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

theorem image_comp : image (R ○ S) s = image S (image R s) := by aesop

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