Mathlib v3 is deprecated. Go to Mathlib v4

Theorem setoid.is_partition.sUnion_eq_univ

Modification history

2020-06-28 06:01
src/data/setoid/partition.lean
feat(subtype): standardize (#3204) …
Modified setoid.is_partition.sUnion_eq_univView on Github →
2020-06-05 05:31
src/data/setoid/partition.lean
feat(data/setoid/partition): some lemmas about partitions (#2937)
Added setoid.is_partition.sUnion_eq_univView on Github →