coe_add

Mathlib.Analysis.Seminorm

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

English

The coercion map respects addition: the coercion of (p+q) equals the sum of the coercions of p and q.

Русский

Сопоставление через коe сохраняет сложение: коe (p+q) = коe p + коe q.

LaTeX

$$$\text{Seminorm.instFunLike.coe} (p + q) = \text{Seminorm.instFunLike.coe} p + \text{Seminorm.instFunLike.coe} q$$$

Lean4

theorem coe_add (p q : Seminorm 𝕜 E) : ⇑(p + q) = p + q :=
  rfl

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

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

Разделы

Аффилиация

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