Theorems · Theorem · logic and foundations

Set.ncard_sdiff

∀ {α : Type u_1} {s t : Set α}, s ⊆ t → autoParam s.Finite Set.ncard_sdiff._auto_1 → (t \ s).ncard = t.ncard - s.ncard

This is the same as ncard_sdiff' but we require s to be finite instead.

Defined in

Mathlib.Data.Set.Card

Cited by

4 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound