English
Every nonempty set s either is finite with a finite encard or has encard top or can be reduced by removing an element.
Русский
Каждое непустое множество S либо имеет конечную encard, либо encard(S) = ⊤, либо его можно уменьшить удалением элемента.
LaTeX
$$$s = \\emptyset \\lor s.encard = \\top \\lor \\exists a \\in s, (s \\setminus \\{a\\}).encard < s.encard$$$
Lean4
theorem encard_eq_three {α : Type u_1} {s : Set α} : encard s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = { x, y, z } :=
by
refine ⟨fun h ↦ ?_, fun ⟨x, y, z, hxy, hyz, hxz, hs⟩ ↦ ?_⟩
· obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
rw [← insert_eq_of_mem hx, ← insert_diff_singleton, encard_insert_of_notMem (fun h ↦ h.2 rfl),
(by exact rfl : (3 : ℕ∞) = 2 + 1), WithTop.add_right_inj WithTop.one_ne_top, encard_eq_two] at h
obtain ⟨y, z, hne, hs⟩ := h
refine ⟨x, y, z, ?_, ?_, hne, ?_⟩
· rintro rfl; exact (hs.symm.subset (Or.inl rfl)).2 rfl
· rintro rfl; exact (hs.symm.subset (Or.inr rfl)).2 rfl
rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]
rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_singleton] <;> aesop
