English
Let P be a predicate on pairs of Finsets. If P is symmetric in its arguments, holds when the second argument is empty, holds for singleton pairs, and is preserved under union in the first argument, then P holds for all pairs of Finsets.
Русский
Пусть P — предикат на парах Finset. Если P симметрична по своим аргументам, выполняется для пары (A, ∅), выполняется для пар вида ({a}, {b}), и сохраняется при объединении в первом аргументе, тогда P выполняется для любых пар Finset.
LaTeX
$$$\\forall P\\,\\Big(\\big(\\forall a,b, P(a,b) \\to P(b,a)\\big) \\land\\big( \\forall a, P(a, \\emptyset) \\big) \\land\\big( \\forall a,b, P\\{a\\},\\{b\\} \\big) \\land\\big( \\forall a,b,c, P(a,c) \\to P(b,c) \\to P(a\\cup b,c) \\big) \\Big) \\to \\forall a,b, P(a,b).$$$
Lean4
@[simp, grind =]
theorem union_insert (a : α) (s t : Finset α) : s ∪ insert a t = insert a (s ∪ t) := by
simp only [insert_eq, union_left_comm]
