English
If a ∉ s and b ∈ s, then encard(insert a (s \\ {b})) = encard(s).
Русский
Если a ∉ s и b ∈ s, тогда encard(insert a (s \\ {b})) = encard(s).
LaTeX
$$((a ∉ s) ∧ (b ∈ s)) ⇒ encard(insert a (s \\ {b})) = encard(s)$$
Lean4
theorem encard_exchange (ha : a ∉ s) (hb : b ∈ s) : (insert a (s \ { b })).encard = s.encard :=
by
rw [encard_insert_of_notMem, encard_diff_singleton_add_one hb]
simp_all only [mem_diff, mem_singleton_iff, false_and, not_false_eq_true]