mem_dom

Mathlib.Data.Rel

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

English

An element a belongs to the domain of R iff there exists b with a ~[R] b.

Русский

Элемент a принадлежит области определения R тогда и только тогда, когда существует b such that a ~[R] b.

LaTeX

$$a \in \operatorname{dom}(R) \iff \exists b, a ~[R] b$$

Lean4

@[simp]
theorem mem_dom : a ∈ R.dom ↔ ∃ b, a ~[R] b :=
  .rfl

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

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

Разделы

Аффилиация

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