join_of_single

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.join_of_single

English

If r is reflexive and a is related to b by r, then there is a join from a to b: Join r a b.

Русский

Если r рефлексивно, и a связано с b через r, существует объединение от a к b: Join r a b.

LaTeX

$$$\\\\operatorname{Join} r a b$$$

Lean4

theorem join_of_single (h : Reflexive r) (hab : r a b) : Join r a b :=
  ⟨b, hab, h b⟩

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

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

Разделы

Аффилиация

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