wbtw

Mathlib.Analysis.Convex.Between

URI: https://scilib.ai/kg/mathlib#Sbtw.wbtw

English

The Sbtw predicate implies the weaker Wbtw predicate: if x, y, z satisfy Sbtw, then x, y, z satisfy Wbtw as well.

Русский

Предикат Sbtw имплицирует более слабый предикат Wbtw: если x, y, z удовлетворяют Sbtw, то они удовлетворяют и Wbtw.

LaTeX

$$$Sbtw R x y z \Rightarrow Wbtw R x y z$$$

Lean4

theorem wbtw {x y z : P} (h : Sbtw R x y z) : Wbtw R x y z :=
  h.1

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

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

Разделы

Аффилиация

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