instSub

Mathlib.Algebra.Order.CauSeq.Basic

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

English

Coordinate-wise subtraction: coe_sub shows (f - g) is computed termwise.

Русский

Вычитание по координатам: coe_sub задаёт (f - g) по каждому члену.

LaTeX

$$$$ \\\\mathrm{coe\\\\_sub}:(f,g) \\\\mapsto (f - g) = (f: \\\\mathbb{N} \\\\to \\\\beta) - g. $$$$

Lean4

instance : Sub (CauSeq β abv) :=
  ⟨fun f g => ofEq (f + -g) (fun x => f x - g x) fun i => by simp [sub_eq_add_neg]⟩

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

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

Разделы

Аффилиация

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