Cardinalities of set differences of finsets

• Finset.card_sdiff_insert_add_one: adding an element a ∈ T \ S to S lowers the number of elements of T outside S by one.
• Finset.subset_induction: downward induction on S ⊆ T, from T itself and steps from S ∪ {a} to S. Mathlib's Finset.induction_on' is the upward analogue.
• Finset.card_sdiff_lt_of_card_eq_min: if F ⊆ U has min k #U elements of a nonempty U and T ⊆ U has fewer than k, then fewer elements of T lie outside F than in F.

theorem Finset.card_sdiff_insert_add_one {ι : Type u_1} [DecidableEq ι] {S T : Finset ι} {a : ι} (ha : a ∈ T \ S) : (T \ insert a S).card + 1 = (T \ S).card

Adding an element a ∈ T \ S to S lowers the number of elements of T outside S by one.

theorem Finset.subset_induction {ι : Type u_1} [DecidableEq ι] {T : Finset ι} {P : (S : Finset ι) → S ⊆ T → Prop} (self : P T ⋯) (step : ∀ (S : Finset ι), ∀ a ∉ S, ∀ (h : insert a S ⊆ T), P (insert a S) h → P S ⋯) (S : Finset ι) (h : S ⊆ T) : P S h

Downward induction on S ⊆ T: a property holding at T, and passing from S ∪ {a} to S, holds for every S ⊆ T.

theorem Finset.card_sdiff_lt_of_card_eq_min {ι : Type u_1} [DecidableEq ι] {F T U : Finset ι} {k : ℕ} (hFU : F ⊆ U) (hTU : T ⊆ U) (hU : U.Nonempty) (hF : F.card = min k U.card) (hT : T.card < k) : (T \ F).card < F.card

If F has min k #U of the elements of a nonempty set U, and T ⊆ U has fewer than k elements, then fewer elements of T lie outside F than in F.