map_disjiUnion — Mathlib

English

Mapping a Finset through an embedding commutes with disjiUnion up to the corresponding mapped fibers.

Русский

Отображение Finset через вложение тегирует дисjoint‑объединение в соответствующих волокнах.

LaTeX

$$$(s.map f).disjiUnion t h = s.disjiUnion (\\lambda a => t (f a)) (\\lambda _ ha _ hb hab => h (mem_map_of_mem _ ha) (mem_map_of_mem _ hb) (f.injective.ne hab))$$$

Lean4

theorem map_disjiUnion {f : α ↪ β} {s : Finset α} {t : β → Finset γ} {h} :
    (s.map f).disjiUnion t h =
      s.disjiUnion (fun a => t (f a)) fun _ ha _ hb hab =>
        h (mem_map_of_mem _ ha) (mem_map_of_mem _ hb) (f.injective.ne hab) :=
  eq_of_veq <| Multiset.bind_map _ _ _

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