tprod_dite_right — Mathlib

English

If P is a proposition and x : β → (¬P → α), then ∏' b, (if P then 1 else x b h) = (if P then 1 else ∏' b, x b h).

Русский

Если P — предложение, и x: β → (¬P → α), то т-произведение над условием равно условному произведению по правая часть.

LaTeX

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

Lean4

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

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