English
The union with the empty set is the original set.
Русский
Объединение с пустым множеством дает исходное множество.
LaTeX
$$$\\emptyset \\cup s = s$$$
Lean4
/-- To prove a relation on pairs of `Finset X`, it suffices to show that it is
* symmetric,
* it holds when one of the `Finset`s is empty,
* it holds for pairs of singletons,
* if it holds for `[a, c]` and for `[b, c]`, then it holds for `[a ∪ b, c]`.
-/
theorem induction_on_union (P : Finset α → Finset α → Prop) (symm : ∀ {a b}, P a b → P b a) (empty_right : ∀ {a}, P a ∅)
(singletons : ∀ {a b}, P { a } { b }) (union_of : ∀ {a b c}, P a c → P b c → P (a ∪ b) c) : ∀ a b, P a b :=
by
intro a b
refine Finset.induction_on b empty_right fun x s _xs hi => symm ?_
rw [Finset.insert_eq]
apply union_of _ (symm hi)
refine Finset.induction_on a empty_right fun a t _ta hi => symm ?_
rw [Finset.insert_eq]
exact union_of singletons (symm hi)
