instNeg

Mathlib.Data.Holor

URI: https://scilib.ai/kg/mathlib#Holor.instNeg

English

For holors, negation is defined pointwise: (-a)(t) = -a(t).

Русский

Для холоров отрицание определяется точечно: (-a)(t) = -a(t).

LaTeX

$$$\forall a:\ Holor\ α\ ds,\ \forall t:\ HolorIndex\ ds,\ (-a)\,t = -(a\,t)$$$

Lean4

instance [Neg α] : Neg (Holor α ds) :=
  ⟨fun a t => -a t⟩

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

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

Разделы

Аффилиация

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