collapse_eq — Mathlib

English

The collapse function has a precise decomposition: for ha, the value equals the sum of two contributions based on membership of s and insert a in s into 𝒜.

Русский

Сollapse распадается на две части в зависимости от принадлежности s и вставки a в s в 𝒜.

LaTeX

$$collapse 𝒜 a f s = (if s∈𝒜 then f s else 0) + (if insert a s ∈ 𝒜 then f (insert a s) else 0)$$

Lean4

theorem collapse_eq (ha : a ∉ s) (𝒜 : Finset (Finset α)) (f : Finset α → β) :
    collapse 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0 :=
  by
  rw [collapse, filter_collapse_eq ha]
  split_ifs <;> simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

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