Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-10 07:36 48104c3a

View on Github →

feat(data/set/lattice): (b)Union and (b)Inter lemmas (#7557) from LTE

Estimated changes

Modified src/data/set/lattice.lean

added theorem set.Union_prop

added theorem set.Union_prop_neg

added theorem set.Union_prop_pos

added theorem set.bInter_inter

added theorem set.inter_bInter

added theorem set.mem_bUnion_iff'