encard_exchange — Mathlib

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]

Похожие утверждения