comp_iUnion — Mathlib

English

If (R_i) is a family of relations from α to β and S is a relation from β to γ, then the composition distributes over the index: (⋃ i, R_i) ○ S = ⋃ i, (R_i ○ S).

Русский

Если (R_i) — семейство отношений α→β и S — отношение β→γ, то композиция распределяется по индексу: (⋃ 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 comp_iUnion (R : SetRel α β) (S : ι → SetRel β γ) : R ○ ⋃ i, S i = ⋃ i, R ○ S i := by aesop

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