isSymmetricRel_idRel

Mathlib.Topology.UniformSpace.Defs

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

English

The identity relation idRel is symmetric.

Русский

Тождественное отношение idRel симметрично.

LaTeX

$$IsSymmetricRel idRel$$

Lean4

theorem isSymmetricRel_idRel : IsSymmetricRel (idRel : Set (α × α)) := by simp [IsSymmetricRel, idRel, eq_comm]

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

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

Разделы

Аффилиация

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