mk_sub

Mathlib.Data.DFinsupp.Defs

URI: https://scilib.ai/kg/mathlib#DFinsupp.mk_sub

← MathLib Explorer

English

Same as Mk Sub above; mk s (x − y) = mk s x − mk s y.

Русский

Повторение того же утверждения: mk s (x − y) = mk s x − mk s y.

LaTeX

$$$ mk s (x - y) = mk s x - mk s y $$$

Lean4

@[simp]
theorem mk_sub [∀ i, AddGroup (β i)] {s : Finset ι} {x y : ∀ i : (↑s : Set ι), β i.1} :
    mk s (x - y) = mk s x - mk s y :=
  ext fun i => by simp only [sub_apply, mk_apply]; split_ifs <;> [rfl; rw [sub_zero]]

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

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

Разделы

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

Аффилиация

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