fromRel — Mathlib

English

Given a symmetric relation r on α, Sym2.fromRel r is the set of unordered pairs {a,b} with r(a,b).

Русский

Для симметричной отношения r на α множество Sym2.fromRel r состоит из неупорядоченных пар {a,b}, удовлетворяющих r(a,b).

LaTeX

$$$$ \mathrm{Sym2.fromRel}(r) = \{ z \in \mathrm{Sym2}(\alpha) \mid r(z.fst,z.snd) \}. $$$$

Lean4

/-- Symmetric relations define a set on `Sym2 α` by taking all those pairs
of elements that are related.
-/
def fromRel (sym : Symmetric r) : Set (Sym2 α) :=
  setOf (lift ⟨r, fun _ _ => propext ⟨(sym ·), (sym ·)⟩⟩)

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