Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-12 02:18 6ca1a09b

View on Github →

refactor(order/bounded_order): relax typeclass requirements on disjoint and codisjoint (#16434) Currently we have two different notions of finset disjointness:

  • ∀ a ∈ s, a ∉ t, used by finset.disj_union and finset.disj_Union
  • disjoint s t (s ⊓ t ≤ ⊥), used by almost everything else The second spelling uses finset.has_inf which requires decidable equality to compute the intersection. Of course, we don't need to compute the intersection, we just need to say that no element can belong to it. More precisely, decidability of equality is only needed for decidability of disjointness, not to state disjointness in the first place. If were were to change finset.disj_union to take a disjoint argument, then either:
  • It would need to be a weird @disjoint term with a classical decidable instance. reducing the generality of the lemma.
  • it would need to gain a decidable_eq argument; thus losing much of the benefit it provides over finset.has_union! Instead, this PR opts for redefining disjoint s t to not require has_inf, as ∀ ⦃x⦄, x ≤ s → x ≤ t → x ≤ ⊥. The analogous change is made to codisjoint s t for consistency. As a bonus, the new definition works in cases where there is no unique infimum. The changes in this PR are largely either:
  • Adjustments to the disjoint API to handle the extra generality
  • Adjustments to proofs that relied on the definitional equality of disjoint to use disjoint.le_bot or disjoint_left
  • Reordering of finset lemmas to move statements about disjointness earlier in the file where no decidable_eq hypothesis is present.

Estimated changes

modified theorem disjoint.of_image_finset
modified theorem finset.bot_eq_empty
modified def finset.disj_union
modified theorem finset.disj_union_comm
modified theorem finset.disj_union_empty
modified theorem finset.disj_union_singleton
modified theorem finset.disjoint_image
modified theorem finset.disjoint_map
modified theorem finset.empty_disj_union
modified theorem finset.filter_disj_union
modified theorem finset.map_disj_union'
modified theorem finset.map_disj_union
deleted theorem finset.map_disj_union_aux
modified theorem finset.singleton_disj_union
modified theorem finsupp.disjoint_iff
modified theorem finsupp.support_inf
modified theorem finsupp.support_sup
modified theorem set.to_finset_disjoint_iff
modified theorem set.disjoint_left
modified theorem disjoint_inf_sdiff
modified theorem disjoint_sdiff_sdiff
modified theorem disjoint_sdiff_self_left
modified theorem disjoint_sdiff_self_right
modified theorem bot_codisjoint
modified theorem codisjoint.comm
modified theorem codisjoint.eq_top
modified theorem codisjoint.eq_top_of_ge
modified theorem codisjoint.eq_top_of_le
modified theorem codisjoint.mono_left
modified theorem codisjoint.mono_right
added theorem codisjoint.top_le
modified def codisjoint
modified theorem codisjoint_bot
modified theorem codisjoint_iff
added theorem codisjoint_iff_le_sup
modified theorem codisjoint_self
modified theorem codisjoint_top_left
modified theorem codisjoint_top_right
modified theorem disjoint.comm
modified theorem disjoint.eq_bot
added theorem disjoint.le_bot
modified def disjoint
modified theorem disjoint_bot_left
modified theorem disjoint_bot_right
modified theorem disjoint_iff
added theorem disjoint_iff_inf_le
modified theorem disjoint_self
modified theorem disjoint_top
modified theorem is_compl.left_le_iff
modified theorem is_compl.of_eq
added theorem is_compl.of_le
modified theorem is_compl.right_le_iff
modified structure is_compl
modified theorem top_disjoint
modified theorem codisjoint_hnot_right
modified theorem disjoint_compl_left
modified theorem hnot_sup_self
modified theorem sup_hnot_self