symmetric_symmetrizeRel

Mathlib.Topology.UniformSpace.Defs

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

← MathLib Explorer

English

The symmetrized relation is symmetric: IsSymmetricRel (symmetrizeRel V).

Русский

Симметризованное отношение симметрично: IsSymmetricRel (symmetrizeRel V).

LaTeX

$$IsSymmetricRel (\mathrm{symmetrizeRel}(V))$$

Lean4

theorem symmetric_symmetrizeRel (V : Set (α × α)) : IsSymmetricRel (symmetrizeRel V) := by
  simp [IsSymmetricRel, symmetrizeRel, preimage_inter, inter_comm, ← preimage_comp]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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