wbtw_nil

Mathlib.Analysis.Convex.BetweenList

URI: https://scilib.ai/kg/mathlib#List.wbtw_nil

English

Let R be a ring and the list of points be empty. Then the empty list satisfies the Wbtw relation, i.e. Wbtw(R, []) holds.

Русский

Пусть R — кольцо, а список точек пуст. Тогда пустой список удовлетворяет отношению Wbtw: Wbtw(R, []).

LaTeX

$$$Wbtw(R,\\,[])$$$

Lean4

@[simp]
theorem wbtw_nil : ([] : List P).Wbtw R := by simp [List.Wbtw]

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

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

Разделы

Аффилиация

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