instSub

Mathlib.Topology.Algebra.ContinuousAffineMap

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

English

There is a subtraction operation on continuous affine maps defined pointwise: (f - g)(x) = f(x) - g(x).

Русский

Существуют вычитание отображений, задаваемые по точкам: (f − g)(x) = f(x) − g(x).

LaTeX

$$$ (f - g)(x) = f(x) - g(x) $$$

Lean4

instance : Sub (P →ᴬ[R] W) where
  sub f g := { (f : P →ᵃ[R] W) - (g : P →ᵃ[R] W) with cont := f.continuous.sub g.continuous }

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

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

Разделы

Аффилиация

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