biUnion_singleton_eq_self — Mathlib

English

The biUnion over a singleton-valued function yields the original set: s.biUnion (singleton : α → Finset α) = s.

Русский

BiUnion над отображением в единичное множество возвращает исходное множество: s.biUnion (singleton : α → Finset α) = s.

LaTeX

$$$\\mathrm{biUnion}(s,\\mathrm{singleton}) = s$$$

Lean4

@[simp]
theorem biUnion_singleton_eq_self [DecidableEq α] : s.biUnion (singleton : α → Finset α) = s := by grind

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