restrictDomain

Mathlib.Data.Rel

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

English

RestrictDomain(R, s) yields the relation on s to β consisting of pairs (a,b) with a ∈ s and a ~R b.

Русский

RestrictDomain(R, s) задаёт отношение на подмножество s к β: пары (a,b) с a ∈ s и a ~R b.

LaTeX

$$\mathrm{restrictDomain}(R, s) = \{(a,b) \mid a \in s \land a ~[R] b\}$$

Lean4

/-- Restrict the domain of a relation to a subtype. -/
def restrictDomain : SetRel s β :=
  {(a, b) | ↑a ~[R] b}

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

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

Разделы

Аффилиация

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