Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-17 08:42 a88ae0c4

View on Github →

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₂.

Estimated changes

modified theorem convex_cone.mem_Inf
added theorem set.mem_Inter₂
added theorem set.mem_Union₂
deleted theorem set.mem_bInter_iff
deleted theorem set.mem_bUnion_iff'
deleted theorem set.mem_bUnion_iff
modified theorem subgroup.mem_Inf
modified theorem submonoid.mem_Inf
modified theorem submodule.mem_span
modified theorem subring.mem_Inf
modified theorem subsemiring.mem_Inf