mem_cod

Mathlib.Data.Rel

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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