interedges — Mathlib

English

Interedges between two finsets is the finite set of all ordered vertex pairs with the first in the first set and the second in the second set that satisfy the relation.

Русский

Межребра между двумя конечными множествами — множество упорядоченных пар вершин, первая из которых принадлежит первому множеству, вторая — второму, удовлетворяющих relation.

LaTeX

$$$\operatorname{interedges}(r, s, t) = \{(x,y) \in s \times t : r(x,y)\}$$$

Lean4

/-- Finset of edges of a relation between two finsets of vertices. -/
def interedges (s t : Finset α) : Finset (α × α) :=
  Rel.interedges G.Adj s t

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