Commit 2024-03-07 15:09 0eaff363

View on Github →

chore(Order): Make more arguments explicit (#11033) Those lemmas have historically been very annoying to use in rw since all their arguments were implicit. One too many people complained about it on Zulip, so I'm changing them. Downstream code broken by this change can fix it by adding appropriately many _s. Also marks CauSeq.ext @[ext].

Order.BoundedOrder

  • top_sup_eq
  • sup_top_eq
  • bot_sup_eq
  • sup_bot_eq
  • top_inf_eq
  • inf_top_eq
  • bot_inf_eq
  • inf_bot_eq

Order.Lattice

  • sup_idem
  • sup_comm
  • sup_assoc
  • sup_left_idem
  • sup_right_idem
  • inf_idem
  • inf_comm
  • inf_assoc
  • inf_left_idem
  • inf_right_idem
  • sup_inf_left
  • sup_inf_right
  • inf_sup_left
  • inf_sup_right

Order.MinMax

  • max_min_distrib_left
  • max_min_distrib_right
  • min_max_distrib_left
  • min_max_distrib_right

Estimated changes

modified theorem CauSeq.ext
modified theorem oneLePart_one
modified theorem Finset.inter_left_idem
modified theorem Finset.inter_right_idem
modified theorem Finset.union_assoc
modified theorem Finset.union_comm
modified theorem Finset.union_idempotent
modified theorem Finset.union_left_idem
modified theorem Finset.union_right_idem
modified theorem Finset.infs_assoc
modified theorem Finset.infs_comm
modified theorem Finset.subset_infs_self
modified theorem Finset.subset_sups_self
modified theorem Finset.sups_assoc
modified theorem Finset.sups_comm
modified theorem Multiset.inter_comm
modified theorem Multiset.union_comm
modified theorem Multiset.inf_singleton
modified theorem Multiset.sup_singleton
modified theorem Set.inter_univ
modified theorem Set.union_univ
modified theorem Set.univ_inter
modified theorem Set.univ_union
modified theorem Set.image_sup_prod
modified theorem Set.infs_assoc
modified theorem Set.infs_comm
modified theorem Set.subset_infs_self
modified theorem Set.subset_sups_self
modified theorem Set.sups_assoc
modified theorem Set.sups_comm
modified theorem compl_sup_eq_top
modified theorem bot_inf_eq
modified theorem bot_sup_eq
modified theorem inf_bot_eq
modified theorem inf_top_eq
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
modified theorem sup_bot_eq
modified theorem sup_top_eq
modified theorem top_inf_eq
modified theorem top_sup_eq
modified theorem eq_top_of_isCompl_bot
modified theorem Coheyting.boundary_bot
modified def InfHom.const
modified def SupHom.const
modified theorem eq_of_inf_eq_sup_eq
modified theorem inf_assoc
modified theorem inf_comm
modified theorem inf_idem
modified theorem inf_left_idem
modified theorem inf_right_idem
modified theorem inf_sup_left
modified theorem inf_sup_right
modified theorem sup_assoc
modified theorem sup_comm
modified theorem sup_idem
modified theorem sup_inf_left
modified theorem sup_inf_right
modified theorem sup_left_idem
modified theorem sup_right_idem
modified theorem max_min_distrib_left
modified theorem max_min_distrib_right
modified theorem min_max_distrib_left
modified theorem min_max_distrib_right