prod_Prop

Mathlib.Algebra.BigOperators.Group.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Fintype.prod_Prop

English

Let f: Prop → M. Then ∏ p, f(p) = f(True) · f(False).

Русский

Пусть f: Prop → M. Тогда ∏ p, f(p) = f(True) · f(False).

LaTeX

$$$$\\prod_{p} f(p) = f(True) \\cdot f(False)$$$$

Lean4

@[to_additive]
theorem prod_Prop (f : Prop → M) : ∏ p, f p = f True * f False := by simp

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

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

Разделы

Аффилиация

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