instNeg

Mathlib.Algebra.Order.CauSeq.Basic

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

English

Negation in CauSeq is defined coordinatewise by negating each term: -f is the CauSeq with -f(i).

Русский

Отрицание в CauSeq задаётся по координатам: -f имеет i-й член -f(i).

LaTeX

$$$$ (-f)(i) = -\\,f(i) \\quad \\text{for all } i. $$$$

Lean4

instance : Neg (CauSeq β abv) :=
  ⟨fun f ↦ ⟨-f, f.2.neg⟩⟩

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

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

Разделы

Аффилиация

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