core_id

Mathlib.Data.Rel

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

English

If R is the identity relation, then the core of any set t is t itself: core .id t = t.

Русский

Если R — отношение идентичности, то ядро любого множества t равно самому t: core .id t = t.

LaTeX

$$core_{\mathrm{id}}(t) = t$$

Lean4

@[simp]
theorem core_id : core .id t = t := by aesop

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

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

Разделы

Аффилиация

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