biUnion_insert — Mathlib

English

Inserting an element a into s yields the disjoint union t a with the rest: (insert a s).biUnion t = t a ∪ s.biUnion t.

Русский

Добавление элемента a в s даёт объединение с волокном t a и остальной частью: (insert a s).biUnion t = t a ∪ s.biUnion t.

LaTeX

$$$\\operatorname{biUnion}\\big(\\operatorname{insert} a\\ s\\big)\\ t = t a \\cup (s.biUnion t)$$$

Lean4

@[simp]
theorem biUnion_insert [DecidableEq α] {a : α} : (insert a s).biUnion t = t a ∪ s.biUnion t := by aesop

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