erase_biUnion — Mathlib

English

Erasing an element b from the biUnion is the same as taking the biUnion of erasing b from each component: (s.biUnion f).erase b = s.biUnion (λ x, (f x).erase b).

Русский

Удаление элемента b из BiUnion равно BiUnion со стиранием b внутри каждой компоненты: (s.biUnion f).erase b = s.biUnion (λ x, (f x).erase b).

LaTeX

$$$((s.biUnion f).erase b) = s.biUnion (\\lambda x. (f x).erase b)$$$

Lean4

theorem erase_biUnion (f : α → Finset β) (s : Finset α) (b : β) :
    (s.biUnion f).erase b = s.biUnion fun x ↦ (f x).erase b := by grind

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