English
Every set is either empty, or has maximal encard, or there exists an element whose removal reduces encard.
Русский
Каждое множество либо пусто, либо имеет максимальную encard, либо существует элемент, удаление которого уменьшает encard.
LaTeX
$$$s = \\emptyset \\lor s.encard = \\top \\lor \\exists a \\in s, (s \\setminus \\{a\\}).encard < s.encard$$$
Lean4
/-- Every set is either empty, infinite, or can have its `encard` reduced by a removal. Intended
for well-founded induction on the value of `encard`. -/
theorem eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt (s : Set α) :
s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ { a }).encard < s.encard :=
by
refine
s.eq_empty_or_nonempty.elim Or.inl
(Or.inr ∘ fun ⟨a, ha⟩ ↦ (s.finite_or_infinite.elim (fun hfin ↦ Or.inr ⟨a, ha, ?_⟩) (Or.inl ∘ Infinite.encard_eq)))
rw [← encard_diff_singleton_add_one ha]; nth_rw 1 [← add_zero (encard _)]
exact WithTop.add_lt_add_left hfin.diff.encard_lt_top.ne zero_lt_one
