mem_comp

Mathlib.Data.Rel

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

English

A relation a ~[R ○ S] c holds if and only if there exists a b such that a ~[R] b and b ~[S] c.

Русский

Отношение a ~[R ○ S] c выполняется тогда, когда существует b, что a ~[R] b и b ~[S] c.

LaTeX

$$a ~[R \circ S] c \iff \exists b, a ~[R] b \land b ~[S] c$$

Lean4

@[simp]
theorem mem_comp : a ~[R ○ S] c ↔ ∃ b, a ~[R] b ∧ b ~[S] c :=
  .rfl

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

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

Разделы

Аффилиация

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