coe_injective

Mathlib.Analysis.BoxIntegral.Partition.Additive

URI: https://scilib.ai/kg/mathlib#BoxIntegral.BoxAdditiveMap.coe_injective

English

The scalar action defined on box-additive maps is injective in its argument, i.e., if r·f = r·g for all boxes, then f = g.

Русский

У кглассного действия на отображенияхBoxAdditiveMap-инъективно по аргументу.

LaTeX

$$$\text{Injective }(f \mapsto (I \mapsto f(I)))$$$

Lean4

theorem coe_injective : Injective fun (f : ι →ᵇᵃ[I₀] M) x => f x :=
  DFunLike.coe_injective

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

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

Разделы

Аффилиация

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