dom

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.dom

English

Domain of a relation R is the set of elements a for which there exists b with a ~[R] b.

Русский

Область определения отношения R — множество тех a, для которых существует b, что a ~[R] b.

LaTeX

$$$\operatorname{dom}(R) = \{ a \in \alpha \mid \exists b \in \beta, a ~[R] b \}$$$

Lean4

/-- Domain of a relation. -/
def dom : Set α :=
  {a | ∃ b, a ~[R] b}

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

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

Разделы

Аффилиация

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