disjiUnion_val — Mathlib

English

The underlying multiset of disjiUnion s t is the bind of s with the underlying multisets of t; i.e., its first projection equals s.1.bind (λ a, (t a).1).

Русский

Основанная на множестве структура disjiUnion имеет вид s.1.bind (λ a, (t a).1).

LaTeX

$$$ (s.disjiUnion t h).1 = s.1.bind (fun a \\rightarrow (t a).1)$$$

Lean4

@[simp]
theorem disjiUnion_val (s : Finset α) (t : α → Finset β) (h) : (s.disjiUnion t h).1 = s.1.bind fun a ↦ (t a).1 :=
  rfl

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