iUnion_comp — Mathlib

English

For a family of relations R_i: SetRel α β and S: SetRel β γ, the composition with their union equals the union of the compositions: (⋃ i, R_i) ○ S = ⋃ i, R_i ○ S.

Русский

Для семейства отношений R_i: SetRel α β и S: SetRel β γ композиция с их объединением равна объединению композиций: (⋃ i, R_i) ○ S = ⋃ i, R_i ○ S.

LaTeX

$$$\Big( \bigcup_i R_i \Big) \circ S = \bigcup_i (R_i \circ S)$$$

Lean4

theorem iUnion_comp (R : ι → SetRel α β) (S : SetRel β γ) : (⋃ i, R i) ○ S = ⋃ i, R i ○ S := by aesop

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