Commit 2026-10-02 21:33 d8440dec

View on Github →

feat(Data/Set/Card): cardinality of complement and difference (#43424)

ncard_compl doesn't need sᶜ.Finite
added sᶜ.encard lemma
added [e]ncard (t \ s) lemmas that don't require s ⊆ t
tag them simp

Estimated changes

Modified Mathlib/Basic/ENNReal/Operations.lean

deleted theorem ENNReal.addLECancellable_iff_ne

added theorem ENNReal.addLECancellable_iff_ne_top

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.addLECancellable_iff_ne_top

Modified Mathlib/Data/Set/Card.lean

modified theorem Set.encard_add_encard_compl

added theorem Set.encard_compl

added theorem Set.encard_sdiff'

added theorem Set.even_ncard_compl_iff'

modified theorem Set.ncard_compl

modified theorem Set.ncard_compl_of_ncard_eq_add

added theorem Set.ncard_pair_eq_two_iff

added theorem Set.ncard_sdiff''

modified theorem Set.ncard_sdiff_singleton_of_mem

added theorem Set.odd_ncard_compl_iff'

Modified Mathlib/Data/Set/Finite/Basic.lean

added theorem Set.Infinite.to_type

Modified Mathlib/Data/Set/PowersetCard.lean

Modified Mathlib/GroupTheory/Perm/MaximalSubgroups.lean

Modified Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean