Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-24 10:24 9870d138

View on Github →

chore(order/bounded_order): Golf disjoint API (#14194) Reorder lemmas and golf. Lemma additions:

  • disjoint.eq_bot_of_ge
  • is_compl.of_dual
  • is_compl_to_dual_iff
  • is_compl_of_dual_iff Lemma deletions:
  • eq_bot_of_disjoint_absorbs: This is an unhelpful combination of disjoint.eq_bot_of_ge and sup_eq_left
  • inf_eq_bot_iff_le_compl: This is a worse version of is_compl.disjoint_left_iff Lemma renames:
  • is_compl.to_order_dual → is_compl.dual

Estimated changes

modified theorem disjoint.comm
modified theorem disjoint.eq_bot
added theorem disjoint.eq_bot_of_ge
modified theorem disjoint.eq_bot_of_le
modified theorem disjoint.inf_left'
modified theorem disjoint.inf_left
modified theorem disjoint.inf_right'
modified theorem disjoint.inf_right
modified theorem disjoint.mono
modified theorem disjoint.mono_left
modified theorem disjoint.mono_right
modified theorem disjoint.ne
modified theorem disjoint.symm
modified theorem disjoint_assoc
modified theorem disjoint_bot_left
modified theorem disjoint_bot_right
modified theorem disjoint_iff
modified theorem disjoint_self
modified theorem eq_bot_of_is_compl_top
modified theorem eq_bot_of_top_is_compl
modified theorem eq_top_of_bot_is_compl
modified theorem eq_top_of_is_compl_bot
deleted theorem inf_eq_bot_iff_le_compl
added theorem is_compl.dual
modified theorem is_compl.left_le_iff
added theorem is_compl.of_dual
modified theorem is_compl.of_eq
deleted theorem is_compl.to_order_dual
modified theorem is_compl_bot_top
added theorem is_compl_of_dual_iff
added theorem is_compl_to_dual_iff
modified theorem is_compl_top_bot
modified theorem max_bot_left
modified theorem max_bot_right
modified theorem max_top_left
modified theorem max_top_right
modified theorem min_bot_left
modified theorem min_bot_right
modified theorem min_top_left
modified theorem min_top_right