comp_sUnion

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.comp_sUnion

English

Let R: SetRel α β and 𝒮: Set (SetRel β γ). Then R ○ ⋃₀ 𝒮 = ⋃_{S ∈ 𝒮} (R ○ S).

Русский

Пусть R: SetRel α β и 𝒮: Set (SetRel β γ). Тогда R ○ ⋃₀ 𝒮 = ⋃_{S ∈ 𝒮} (R ○ S).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru