biUnion_biUnion — Mathlib

English

BiUnion distributes over another BiUnion: (s.biUnion f).biUnion g = s.biUnion (λ a, (f a).biUnion g).

Русский

BiUnion распределяется над другим BiUnion: (s.biUnion f).biUnion g = s.biUnion (λ a, (f a).biUnion g).

LaTeX

$$$(s.biUnion f).biUnion g = s.biUnion (\\lambda a \\mapsto (f a).biUnion g)$$$

Lean4

theorem biUnion_biUnion [DecidableEq γ] (s : Finset α) (f : α → Finset β) (g : β → Finset γ) :
    (s.biUnion f).biUnion g = s.biUnion fun a ↦ (f a).biUnion g := by grind

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