id_compRel

Mathlib.Topology.UniformSpace.Defs

URI: https://scilib.ai/kg/mathlib#id_compRel

English

Left identity for relation composition: idRel ∘ r = r.

Русский

Левая единица для композиции отношений: idRel ∘ r = r.

LaTeX

$$$\mathrm{idRel} \circ r = r$$$

Lean4

@[simp]
theorem id_compRel {r : Set (α × α)} : idRel ○ r = r :=
  Set.ext fun ⟨a, b⟩ => by simp

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

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

Разделы

Аффилиация

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