of_le_of_le

Mathlib.Analysis.Convex.Between

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

English

If x ≤ y ≤ z in a linearly ordered setting, then Wbtw R x y z holds.

Русский

Если x ≤ y ≤ z на линейно упорядоченном множестве, то выполняется Wbtw R x y z.

LaTeX

$$Wbtw(R,x,y,z) ⟺ x ≤ y ∧ y ≤ z$$

Lean4

theorem of_le_of_le {x y z : R} (hxy : x ≤ y) (hyz : y ≤ z) : Wbtw R x y z :=
  (wbtw_iff_of_le (hxy.trans hyz)).mpr ⟨hxy, hyz⟩

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

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

Разделы

Аффилиация

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