preimage_comp — Mathlib

English

For any R, S, and u, the preimage under the composition equals the preimage under R of the preimage under S of u: preimage (R ○ S) u = preimage R (preimage S u).

Русский

Предобраз композиции равен предобразу R от предобраза S от u.

LaTeX

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

Lean4

theorem preimage_comp : preimage (R ○ S) u = preimage R (preimage S u) := by aesop

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