mk_mem_comm

Mathlib.Topology.UniformSpace.Defs

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

English

For symmetric V, (x,y) ∈ V iff (y,x) ∈ V.

Русский

Для симметричного V: (x,y) ∈ V эквивалентно (y,x) ∈ V.

LaTeX

$$$(x,y) \in V \iff (y,x) \in V$$$

Lean4

theorem mk_mem_comm {V : Set (α × α)} (hV : IsSymmetricRel V) {x y : α} : (x, y) ∈ V ↔ (y, x) ∈ V :=
  Set.ext_iff.1 hV (y, x)

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

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

Разделы

Аффилиация

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