Commit 2025-12-24 12:03 78bd64de

View on Github →

feat(Order/Disjoint): use @[to_dual] (#33140) This PR continues tagging things with @[to_dual], in particular stuff about Disjoint/Codisjoint. New declarations introduced by this PR:

  • codisjoint_of_subsingleton
  • Disjoint.ne_top_of_ne_bot
  • sup_lt_right_of_left_ne_bot

Estimated changes

deleted theorem Codisjoint.dual
deleted theorem Codisjoint.eq_iff
deleted theorem Codisjoint.eq_top
deleted theorem Codisjoint.eq_top_of_ge
deleted theorem Codisjoint.eq_top_of_le
deleted theorem Codisjoint.mono
deleted theorem Codisjoint.mono_left
deleted theorem Codisjoint.mono_right
deleted theorem Codisjoint.ne
deleted theorem Codisjoint.ne_iff
deleted theorem Codisjoint.out
deleted theorem Codisjoint.sup_left'
deleted theorem Codisjoint.sup_left
deleted theorem Codisjoint.sup_right'
deleted theorem Codisjoint.sup_right
deleted theorem Codisjoint.symm
deleted theorem Codisjoint.top_le
deleted def Codisjoint
modified theorem Disjoint.eq_iff
modified theorem Disjoint.mono
modified theorem Disjoint.ne_iff
deleted theorem IsCompl.sup_eq_top
deleted theorem bot_codisjoint
deleted theorem codisjoint_assoc
deleted theorem codisjoint_bot
deleted theorem codisjoint_comm
deleted theorem codisjoint_iff
deleted theorem codisjoint_iff_le_sup
deleted theorem codisjoint_left_comm
deleted theorem codisjoint_ofDual_iff
deleted theorem codisjoint_right_comm
deleted theorem codisjoint_self
deleted theorem codisjoint_toDual_iff
deleted theorem codisjoint_top_left
deleted theorem codisjoint_top_right
deleted theorem symmetric_codisjoint