tprod_dite_left — Mathlib

English

For a proposition P and x: β → P → α, we have ∏' b, (if P then x b h else 1) = (if P then ∏' b, x b h else 1).

Русский

Для предложения P и функции x: β → P → α имеет место т-произведение с условием слева соответствует условному произведению справа.

LaTeX

$$$\\\\prod' b, (if h : P then x b h else 1) = if h : P then \\\\prod' b, x b h else 1$$$

Lean4

@[to_additive]
theorem tprod_dite_left (P : Prop) [Decidable P] (x : β → P → α) :
    ∏'[L] b, (if h : P then x b h else 1) = if h : P then ∏'[L] b, x b h else 1 := by by_cases hP : P <;> simp [hP]

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