Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.intersecting.disjoint_map_compl

Modification history

2022-11-12 02:18
src/combinatorics/set_family/intersecting.lean
refactor(order/bounded_order): relax typeclass requirements on `disjoint` and `codisjoint` (#16434) …
Modified set.intersecting.disjoint_map_complView on Github →
2022-11-06 11:48
src/combinatorics/set_family/intersecting.lean
chore(combinatorics/set_family/intersecting): extract a repeated proof into a lemma (#17371)
Added set.intersecting.disjoint_map_complView on Github →