core_inter

Mathlib.Data.Rel

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

English

The core of an intersection equals the intersection of the cores: R.core(t1 ∩ t2) = (R.core t1) ∩ (R.core t2).

Русский

Ядро пересечения равно пересечению ядер: R.core(t1 ∩ t2) = (R.core t1) ∩ (R.core t2).

LaTeX

$$R.\mathrm{core}(t_1 \cap t_2) = R.\mathrm{core}(t_1) \cap R.\mathrm{core}(t_2)$$

Lean4

theorem core_inter : R.core (t₁ ∩ t₂) = R.core t₁ ∩ R.core t₂ := by aesop

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

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

Разделы

Аффилиация

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