English
The encard equality with add-one characterizes a decomposition s = insert a t with t.encard = k and a ∉ t.
Русский
Равенство encard(S) = k + 1 эквивалентно существованию разложения S = insert a t с t.encard = k и a ∉ t.
LaTeX
$$$encard(s) = k + 1 \\iff \\exists a\\ t, a \\notin t \\land insert a t = s \\land t.encard = k$$$
Lean4
theorem encard_eq_two : s.encard = 2 ↔ ∃ x y, x ≠ y ∧ s = { x, y } :=
by
refine ⟨fun h ↦ ?_, fun ⟨x, y, hne, hs⟩ ↦ by rw [hs, encard_pair hne]⟩
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), ← one_add_one_eq_two,
WithTop.add_right_inj (WithTop.one_ne_top), encard_eq_one] at h
obtain ⟨y, h⟩ := h
refine ⟨x, y, by rintro rfl; exact (h.symm.subset rfl).2 rfl, ?_⟩
rw [← h, insert_diff_singleton, insert_eq_of_mem hx]
