Commit 2024-10-18 02:46 1814dc4d

View on Github →

refactor(Equiv/Set): use Disjoint (#17880) ... instead of s ∩ t ⊆ ∅ in Equiv.Set.union. Also add simps to Equiv.Set.univ.

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/GroupTheory/Perm/Finite.lean

Modified Mathlib/Logic/Equiv/Set.lean

modified theorem Equiv.Set.union_apply_left

modified theorem Equiv.Set.union_apply_right

modified theorem Equiv.Set.union_symm_apply_left

modified theorem Equiv.Set.union_symm_apply_right

Modified Mathlib/SetTheory/Cardinal/Basic.lean