trans

Mathlib.Topology.Connected.PathConnected

URI: https://scilib.ai/kg/mathlib#Joined.trans

English

If x is joined to y and y is joined to z, then x is joined to z via the concatenation of the two paths.

Русский

Если x связано с y и y связано с z, то x связано с z путём конкатенации двух путей.

LaTeX

$$$Joined x y \land Joined y z \Rightarrow Joined x z$$$

Lean4

@[trans]
theorem trans {x y z : X} (hxy : Joined x y) (hyz : Joined y z) : Joined x z :=
  ⟨hxy.somePath.trans hyz.somePath⟩

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

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

Разделы

Аффилиация

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