prodMk_mem_comp

Mathlib.Data.Rel

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

English

If a ~[R] b and b ~[S] c, then a ~[R ○ S] c.

Русский

Если a ~[R] b и b ~[S] c, то a ~[R ○ S] c.

LaTeX

$$a ~[R] b \land b ~[S] c \Rightarrow a ~[R \circ S] c$$

Lean4

theorem prodMk_mem_comp (hab : a ~[R] b) (hbc : b ~[S] c) : a ~[R ○ S] c :=
  ⟨b, hab, hbc⟩

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

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

Разделы

Аффилиация

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