coe_add

Mathlib.Analysis.Normed.Group.Seminorm

URI: https://scilib.ai/kg/mathlib#GroupSeminorm.coe_add

English

The coercion respects addition: the function corresponding to p + q is the sum of the functions of p and q.

Русский

Коэрцирование сохраняет сложение: функция p + q равна сумме функций p и q.

LaTeX

$$⇑(p + q) = ⇑p + ⇑q$$

Lean4

@[to_additive (attr := simp)]
theorem coe_add : ⇑(p + q) = p + q :=
  rfl

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

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

Разделы

Аффилиация

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