indicator_prod_one — Mathlib

English

For t ⊆ κ and j ∈ κ, we have (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i · t.indicator 1 j; i.e., the product indicator on a product set equals the product of the row and column indicators.

Русский

Пусть t ⊆ κ и j ∈ κ. Тогда (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i · t.indicator 1 j.

LaTeX

$$$ (s \times^\mathrm{s} t).indicator 1 \{ fst := i, snd := j \} = s.indicator 1 i \cdot t.indicator 1 j. $$$

Lean4

theorem indicator_prod_one {t : Set κ} {j : κ} :
    (s ×ˢ t).indicator (1 : ι × κ → M₀) (i, j) = s.indicator 1 i * t.indicator 1 j :=
  by
  simp_rw [indicator, mem_prod_eq]
  split_ifs with h₀ <;> simp only [Pi.one_apply, mul_one, mul_zero] <;> tauto

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