sUnion_comp — Mathlib

English

For a set ℛ of SetRel α β and S: SetRel β γ, we have ⋃₀ ℛ ○ S = ⋃_{R ∈ ℛ} (R ○ S).

Русский

Для множества ℛ отношения SetRel α β и S: SetRel β γ выполняется ⋃₀ ℛ ○ S = ⋃_{R ∈ ℛ} (R ○ S).

LaTeX

$$$\bigcup\!_{\mathcal{R}} (\mathcal{R}) \circ S = \bigcup_{R \in \mathcal{R}} (R \circ S)$$$

Lean4

theorem sUnion_comp (ℛ : Set (SetRel α β)) (S : SetRel β γ) : ⋃₀ ℛ ○ S = ⋃ R ∈ ℛ, R ○ S := by aesop

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