ToRel — Mathlib

English

The inverse to Sym2.fromRel: Given a set on Sym2 α, define a symmetric relation on α by xRy if x,y belong to the set element.

Русский

Обратная операция к Sym2.fromRel: множество на Sym2 α задаёт симметричное отношение на α: xRy, если пара x,y принадлежит множеству.

LaTeX

$$$$ \text{ToRel}(s,x,y) := s(x,y) \in s. $$$$

Lean4

/-- The inverse to `Sym2.fromRel`. Given a set on `Sym2 α`, give a symmetric relation on `α`
(see `Sym2.toRel_symmetric`). -/
def ToRel (s : Set (Sym2 α)) (x y : α) : Prop :=
  s(x, y) ∈ s

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