Commit 2021-08-05 19:03 52b6516b

View on Github →

refactor(order/disjointed): generalize disjointed to generalized boolean algebras (#8409)

  • Split data.set.disjointed into data.set.pairwise and order.disjointed. Change imports accordingly.
  • In order.disjointed, change set α to generalized_boolean_algebra α. Redefine disjointed in terms of partial_sups to avoid needing completeness. Keep set notation variants of lemmas for easier unification.
  • Rename some lemmas and reorder their arguments to make dot notation functional.
  • Generalize some (where some = 2) pairwise lemmas.
  • Delete lemmas which are unused and are a straightforward rw away from a simpler one (Union_disjointed_of_mono).

Estimated changes

added theorem Union_disjointed
added theorem disjoint_disjointed
added def disjointed
added theorem disjointed_le
added theorem disjointed_le_id
added def disjointed_rec
added theorem disjointed_rec_zero
added theorem disjointed_subset
added theorem disjointed_succ
added theorem disjointed_unique
added theorem disjointed_zero
added theorem monotone.disjointed_eq
deleted theorem set.Inter_lt_succ
deleted theorem set.Union_disjointed
deleted theorem set.Union_lt_succ
deleted theorem set.disjoint_disjointed'
deleted theorem set.disjoint_disjointed
deleted def set.disjointed
deleted theorem set.disjointed_induct
deleted theorem set.disjointed_of_mono
deleted theorem set.disjointed_subset
added theorem supr_disjointed