Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-18 14:15 6f4aea44

View on Github →

feat(data/set/pairwise): Simple pairwise_disjoint lemmas (#9764)

Estimated changes

Modified src/algebra/support.lean

Modified src/data/finset/basic.lean

modified theorem finset.disjoint_singleton

added theorem finset.disjoint_singleton_left

added theorem finset.disjoint_singleton_right

deleted theorem finset.singleton_disjoint

Modified src/data/finsupp/basic.lean

Modified src/data/polynomial/iterated_deriv.lean

Modified src/data/set/lattice.lean

added theorem set.disjoint_singleton

Modified src/data/set/pairwise.lean

modified theorem set.pairwise_disjoint.elim'

modified theorem set.pairwise_disjoint.elim

added theorem set.pairwise_disjoint.image_of_le

added theorem set.pairwise_disjoint.insert

modified theorem set.pairwise_disjoint.range

modified theorem set.pairwise_disjoint.subset

added theorem set.pairwise_disjoint_empty

added theorem set.pairwise_disjoint_insert

added theorem set.pairwise_disjoint_range_singleton

added theorem set.pairwise_disjoint_singleton

Modified src/geometry/euclidean/circumcenter.lean

Modified src/group_theory/specific_groups/alternating.lean

Modified src/measure_theory/integral/bochner.lean

Modified src/ring_theory/witt_vector/witt_polynomial.lean

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/separation.lean