prod_insertNone

Mathlib.Algebra.BigOperators.Option

URI: https://scilib.ai/kg/mathlib#Finset.prod_insertNone

← MathLib Explorer

English

For f : Option α → M and s : Finset α,

Русский

Для f : Option α → M и s : Finset α

LaTeX

$$$$ \\prod_{x ∈ \\mathrm{insertNone}(s)} f(x) = f(\\mathrm{none}) \\cdot \\prod_{x ∈ s} f(\\mathrm{some}~x). $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_insertNone (f : Option α → M) (s : Finset α) : ∏ x ∈ insertNone s, f x = f none * ∏ x ∈ s, f (some x) := by
  simp [insertNone]

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

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

Разделы

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

Аффилиация

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