symmetrizeRel

Mathlib.Topology.UniformSpace.Defs

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

English

The maximal symmetric relation contained in V is V ∩ Prod.swap ⁻¹' V.

Русский

Максимальная симметричная часть relation внутри V: V ∩ Prod.swap ⁻¹' V.

LaTeX

$$$\mathrm{symmetrizeRel}(V) = V \cap Prod.swap^{-1} V$$$

Lean4

/-- The maximal symmetric relation contained in a given relation. -/
def symmetrizeRel (V : Set (α × α)) : Set (α × α) :=
  V ∩ Prod.swap ⁻¹' V

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

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

Разделы

Аффилиация

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