ite_zero_mul_ite_zero — Mathlib

English

For P,Q propositions and a,b in α, (if P then a else 0) · (if Q then b else 0) = if (P ∧ Q) then a · b else 0.

Русский

Пусть P и Q — высказывания, a,b ∈ α. Тогда (если P, то a, иначе 0) · (если Q, то b, иначе 0) = если P ∧ Q, то a·b, иначе 0.

LaTeX

$$$ \text{ite}(P,a,0) \cdot \text{ite}(Q,b,0) = \text{ite}(P \land Q, a\cdot b, 0) $$$

Lean4

theorem ite_zero_mul_ite_zero : ite P a 0 * ite Q b 0 = ite (P ∧ Q) (a * b) 0 := by
  simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]

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