Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 09:46 b3ad3f2a

View on Github →

feat(data/set/lattice): review (#11672)

  • generalize set.Union_coe_set and set.Inter_coe_set to dependent functions;
  • add bInter_Union, sUnion_Union;
  • drop sUnion_bUnion, sInter_bUnion.

Estimated changes

modified theorem set.Inter_coe_set
modified theorem set.Union_coe_set
added theorem set.bInter_Union
deleted theorem set.sInter_bUnion
added theorem set.sUnion_Union
deleted theorem set.sUnion_bUnion