core_comp

Mathlib.Data.Rel

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

English

The core of a composed relation equals the core of the outer relation applied to the core of the inner: core(R ○ S) u = core(R)(core(S)u).

Русский

Ядро композиции отношений удовлетворяет: core(R ○ S) u = core(R)(core(S) u).

LaTeX

$$R.\mathrm{core}(R \circ S)(u) = R.\mathrm{core}(S.\mathrm{core}(u))$$

Lean4

theorem core_comp : core (R ○ S) u = core R (core S u) := by aesop

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

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

Разделы

Аффилиация

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