map_id_id

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.map_id_id

English

Map r id id = r; i.e., mapping by the identity leaves the relation unchanged.

Русский

Map r id id = r; отображение по тождественному не меняет отношение.

LaTeX

$$$\mathrm{Map}(r,\mathrm{id},\mathrm{id}) = r$$$

Lean4

@[simp]
theorem map_id_id (r : α → β → Prop) : Relation.Map r id id = r := by ext; simp [Relation.Map]

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

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

Разделы

Аффилиация

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