Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-08 10:43 d3bbaeb9

View on Github →

chore(combinatorics/composition): use order_embedding (#5276)

  • use order_embedding for composition.boundary
  • use order_embedding for composition.embedding
  • add max_eq_right_iff etc
  • golf some proofs

Estimated changes

added theorem max_eq_left_iff
added theorem max_eq_right_iff
added theorem min_eq_left_iff
added theorem min_eq_right_iff
modified def composition.boundary
modified def composition.embedding
modified theorem composition.ones_blocks
modified theorem composition.single_blocks
modified theorem composition.single_length