Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-30 05:50 51553e36

View on Github →

chore(data/set/lattice): use dot syntax for disjoint.* (#2282)

Estimated changes

Modified src/data/finsupp.lean

Modified src/data/set/lattice.lean

added theorem disjoint.mono

added theorem disjoint.mono_left

added theorem disjoint.mono_right

added theorem disjoint.ne

deleted theorem disjoint_mono

deleted theorem disjoint_mono_left

deleted theorem disjoint_mono_right

deleted theorem ne_of_disjoint

modified def set.kern_image

added theorem set.pairwise_disjoint.elim

added theorem set.pairwise_disjoint.range

added theorem set.pairwise_disjoint.subset

deleted theorem set.pairwise_disjoint_elim

deleted theorem set.pairwise_disjoint_range

deleted theorem set.pairwise_disjoint_subset

Modified src/data/setoid.lean

Modified src/linear_algebra/basic.lean

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/finsupp.lean

Modified src/linear_algebra/finsupp_vector_space.lean

Modified src/order/conditionally_complete_lattice.lean

Modified src/topology/separation.lean