ncard_exchange' — Mathlib

English

A variant of the exchange operation also preserves cardinality.

Русский

Вариант операции обмена также сохраняет кардинал.

LaTeX

$$$ (insert a\ s \ { b }).ncard = s.ncard $$$

Lean4

theorem ncard_exchange' {a b : α} (ha : a ∉ s) (hb : b ∈ s) : (insert a s \ { b }).ncard = s.ncard := by
  rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib,
    diff_singleton_eq_self fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]

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