English
Let s be a nonempty finite set. Then there exist a finite t and an element a such that s = cons a t ha for some proof ha that a ∉ t. Equivalently, s = insert a t with a ∉ t.
Русский
Пусть s — непустое конечное множество. Тогда существует конечное множество t и элемент a such that s = cons a t ha для некоторого ha: a ∉ t. Эквивалентно: s = insert a t и a ∉ t.
LaTeX
$$$\\displaystyle \\text{If } s \\text{ is a nonempty finite set, then } \\exists t\\,\\exists a\\, (a \\notin t)\\;\\wedge\\; s = \\operatorname{insert} a\, t.$$$
Lean4
theorem exists_cons_eq {α} {s : Finset α} (hs : s.Nonempty) : ∃ t a ha, cons a t ha = s :=
hs.cons_induction (fun a ↦ ⟨∅, a, _, cons_empty _⟩) fun _ _ _ _ _ ↦ ⟨_, _, _, rfl⟩
