Cardinality of a finite set and subtraction

This file contains results on the cardinality of a Finset and subtraction, by casting the cardinality as element of an AddGroupWithOne.

Main results

• Finset.cast_card_erase_of_mem: erasing an element of a finset decrements the cardinality (avoiding ℕ subtraction).
• Finset.cast_card_inter, Finset.cast_card_union: inclusion/exclusion principle.
• Finset.cast_card_sdiff: cardinality of t \ s is the difference of cardinalities if s ⊆ t.

@[simp]

theorem Finset.cast_card_erase_of_mem {α : Type u_1} {a : α} [DecidableEq α] {R : Type u_4} [AddGroupWithOne R] {s : Finset α} (hs : a ∈ s) : ↑(s.erase a).card = ↑s.card - 1

$\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$. This result is casted to any additive group with 1, so that we don't have to work with ℕ-subtraction.

Lattice structure

theorem Finset.cast_card_inter {α : Type u_1} {R : Type u_3} {s t : Finset α} [DecidableEq α] [AddGroupWithOne R] : ↑(s ∩ t).card = ↑s.card + ↑t.card - ↑(s ∪ t).card

theorem Finset.cast_card_union {α : Type u_1} {R : Type u_3} {s t : Finset α} [DecidableEq α] [AddGroupWithOne R] : ↑(s ∪ t).card = ↑s.card + ↑t.card - ↑(s ∩ t).card

theorem Finset.cast_card_sdiff {α : Type u_1} {R : Type u_3} {s t : Finset α} [DecidableEq α] [AddGroupWithOne R] (h : s ⊆ t) : ↑(t \ s).card = ↑t.card - ↑s.card