sbtw

Mathlib.Analysis.Convex.BetweenList

URI: https://scilib.ai/kg/mathlib#List.Sorted.sbtw

English

If l is a list and f is an affine equivalence, then (l.map f).Sbtw R ↔ l.Sbtw R.

Русский

Если l — список и f — аффинное эквивалентное отображение, тогда (l.map f).Sbtw R ↔ l.Sbtw R.

LaTeX

$$$(l.map (EquivLike.toFunLike\\coe f)).Sbtw(R) \\iff l.Sbtw(R)$$$

Lean4

theorem sbtw {l : List R} (h : l.Sorted (· < ·)) : l.Sbtw R :=
  ⟨Sorted.wbtw (h.imp LT.lt.le), h.imp LT.lt.ne⟩

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

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

Разделы

Аффилиация

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