Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-06 21:32 6c23bad2

View on Github →

feat(data/set/lattice): add @[simp] to lemmas (#2091)

  • feat(data/set/lattice): add @[simp] to lemmas
  • fix proof
  • fix proof
  • fix proof
  • oops
  • fix proofs
  • typo in doc string

Estimated changes

modified theorem set.bInter_image
modified theorem set.bInter_range
modified theorem set.bUnion_image
modified theorem set.bUnion_range