card_compl_set — Mathlib

English

The size of the complement equals the universe cardinality minus the size of s, i.e., |s^c| = |α| - |s|.

Русский

Размер дополнения равен размеру вселенной минус размер s, т.е. |s^c| = |α| - |s|.

LaTeX

$$|s^c| = |\alpha| - |s|$$

Lean4

theorem card_compl_set [Fintype α] (s : Set α) [Fintype s] [Fintype (↥sᶜ : Sort _)] :
    Fintype.card (↥sᶜ : Sort _) = Fintype.card α - Fintype.card s := by
  classical rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]

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