eq

Mathlib.Topology.UniformSpace.Defs

URI: https://scilib.ai/kg/mathlib#IsSymmetricRel.eq

English

If U is symmetric, Prod.swap ⁻¹' U = U.

Русский

Если U симметрично, тогда Prod.swap ⁻¹' U = U.

LaTeX

$$$\mathrm{Prod.swap}^{-1} U = U$$$

Lean4

theorem eq {U : Set (α × α)} (hU : IsSymmetricRel U) : Prod.swap ⁻¹' U = U :=
  hU

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

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

Разделы

Аффилиация

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