instAddMonoid

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEEqFun.instAddMonoid

← MathLib Explorer

English

There is an AddMonoid structure on α →ₘ[μ] γ when γ is an AddMonoid with ContinuousAdd.

Русский

Для γ с AddMonoid и ContinuousAdd существует структура AddMonoid на α →ₘ[μ] γ.

LaTeX

$$$\mathrm{AddMonoid}(α \to_{μ} γ)$$$

Lean4

instance instAddMonoid [AddMonoid γ] [ContinuousAdd γ] : AddMonoid (α →ₘ[μ] γ) :=
  toGerm_injective.addMonoid toGerm zero_toGerm add_toGerm fun _ _ => smul_toGerm _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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