disjiUnion_map — Mathlib

English

DisjiUnion is compatible with mapping of the index: mapping the whole disjiUnion over t along f equals the disjiUnion over mapped fibers.

Русский

Совместимо ли disjiUnion с отображением индекса: отображение всего disjiUnion над t через f эквивалентно disjiUnion над отображёнными волокнами.

LaTeX

$$$(s.disjiUnion t h).map f = s.disjiUnion (\\lambda a => (t a).map f) (h.mono' \\; \\text{...})$$$

Lean4

theorem disjiUnion_map {s : Finset α} {t : α → Finset β} {f : β ↪ γ} {h} :
    (s.disjiUnion t h).map f = s.disjiUnion (fun a => (t a).map f) (h.mono' fun _ _ ↦ (disjoint_map _).2) :=
  eq_of_veq <| Multiset.map_bind _ _ _

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