prod_indicator_biUnion_sub_indicator

English

Over a nonempty finite index set, the product of pairwise indicators over a biUnion equals zero: ∏_{i∈s} (1_{⋃ i∈s S_i}(a) − 1_{S_i}(a)) = 0.

Русский

Для непустого конечного множества индексов произведение попарных индикаторных функций над biUnion равно нулю: ∏_{i∈s} (1_{⋃ i∈s S_i}(a) − 1_{S_i}(a)) = 0.

LaTeX

$$$ \prod_{i \in s} \left( \mathbf{1}_{\bigcup_{i \in s} S_i}(a) - \mathbf{1}_{S_i}(a) \right) = 0 $$$

Lean4

theorem prod_indicator_biUnion_sub_indicator (hs : s.Nonempty) (S : ι → Set α) (a : α) :
    ∏ i ∈ s, (Set.indicator (⋃ i ∈ s, S i) 1 a - Set.indicator (S i) 1 a) = (0 : ℤ) :=
  by
  by_cases ha : a ∈ ⋃ i ∈ s, S i
  · have ha' := ha
    simp only [Set.mem_iUnion, exists_prop] at ha
    obtain ⟨i, hi, ha⟩ := ha
    apply prod_eq_zero hi (by simp [ha, ha'])
  · obtain ⟨i, hi⟩ := hs
    have ha : a ∉ S i := by aesop
    exact prod_eq_zero hi <| by simp [*, -coe_biUnion]

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