English
The encard of s equals k + 1 exactly when there exists a with t such that a ∉ t, insert a t = s, and t.encard = k.
Русский
encard(S) = k + 1 тогда и только тогда существуют a и t такие, что a ∉ t, insert a t = s и t.encard = k.
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_add_one_iff {k : ℕ∞} : s.encard = k + 1 ↔ (∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k) :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· obtain ⟨a, ha⟩ := nonempty_of_encard_ne_zero (s := s) (by simp [h])
refine ⟨a, s \ { a }, fun h ↦ h.2 rfl, by rwa [insert_diff_singleton, insert_eq_of_mem], ?_⟩
rw [← WithTop.add_right_inj WithTop.one_ne_top, ← h, encard_diff_singleton_add_one ha]
rintro ⟨a, t, h, rfl, rfl⟩
rw [encard_insert_of_notMem h]
