lattice): Generalize `mem_bUnion_iff` and `mem_bInter_iff` to dependent families (#11485)

Commit

3 years ago

refactor(data/set/lattice): Generalize `mem_bUnion_iff` and `mem_bInter_iff` to dependent families (#11485) They're now called `mem_Union₂` and `mem_Inter₂`.

Author

vihdzp

Parents

83eff323

mathlib3 a88ae0c4 - refactor(data/set/lattice): Generalize `mem_bUnion_iff` and `mem_bInter_iff` to dependent families (#11485)

mathlib3
a88ae0c4 - refactor(data/set/lattice): Generalize `mem_bUnion_iff` and `mem_bInter_iff` to dependent families (#11485)