isSymmetricRel_univ

Mathlib.Topology.UniformSpace.Defs

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

English

The universal relation univ on α is symmetric.

Русский

Универсальное отношение univ на α симметрично.

LaTeX

$$IsSymmetricRel Set.univ$$

Lean4

theorem isSymmetricRel_univ : IsSymmetricRel (Set.univ : Set (α × α)) := by simp [IsSymmetricRel]

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

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

Разделы

Аффилиация

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