trans_right

Mathlib.Analysis.Convex.Between

URI: https://scilib.ai/kg/mathlib#Wbtw.trans_right

English

If Wbtw R w x z and Wbtw R x y z then Sbtw R w y z.

Русский

Если Wbtw R w x z и Wbtw R x y z, то Sbtw R w y z.

LaTeX

$$$$ Wbtw R w x z \to Wbtw R x y z \to Sbtw R w y z $$$$

Lean4

theorem trans_right {w x y z : P} (h₁ : Wbtw R w x z) (h₂ : Wbtw R x y z) : Wbtw R w y z :=
  by
  rw [wbtw_comm] at *
  exact h₁.trans_left h₂

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

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

Разделы

Аффилиация

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