Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 13:11 cf917732

View on Github →

refactor(*): split order_{top,bot} from lattice hierarchy (#9891) Rename bounded_lattice to bounded_order. Split out order_{top,bot} and bounded_order from the order hierarchy. That means that we no longer have semilattice_{sup,inf}_{top,bot}, but use the [order_top] as a mixin to semilattice_inf, for example. Similarly, lattice and bounded_order instead of what was before bounded_lattice. Similarly, distrib_lattice and bounded_order instead of what was before bounded_distrib_lattice.

Estimated changes

modified theorem finset.comp_inf_eq_inf_comp
modified theorem finset.comp_sup_eq_sup_comp
modified theorem finset.disjoint_sup_left
modified theorem finset.disjoint_sup_right
modified theorem finset.sup_finset_image
modified theorem finsupp.support_sup
modified theorem set.Icc_bot_top
modified theorem pairwise_disjoint_on
modified theorem pairwise_disjoint_on_bool
modified theorem is_atom.disjoint_of_ne
modified theorem is_atom.inf_eq_bot_of_ne
modified theorem is_atom_dual_iff_is_coatom
modified theorem is_coatom.sup_eq_top_of_ne
modified theorem is_coatom_dual_iff_is_atom
modified theorem order_iso.is_atom_iff
modified theorem order_iso.is_atomic_iff
modified theorem order_iso.is_coatom_iff
modified theorem order_iso.is_coatomic_iff
modified theorem order_iso.is_simple_lattice
modified theorem pi.le_def
modified theorem pi.compl_apply
deleted theorem bounded_lattice.ext
added theorem bounded_order.ext
modified theorem eq_bot_of_bot_eq_top
modified theorem eq_top_of_bot_eq_top
modified structure is_compl
modified theorem is_compl_bot_top
modified theorem is_compl_top_bot
modified theorem order_bot.ext
modified theorem order_bot.ext_bot
modified theorem order_top.ext
modified theorem subsingleton_iff_bot_eq_top
modified theorem subsingleton_of_bot_eq_top
modified theorem subsingleton_of_top_le_bot
added def lattice.copy
modified def set.Icc.order_bot
modified def set.Icc.order_top
modified theorem partial_sups_eq_sup_range
modified theorem disjoint.map_order_iso
modified theorem disjoint_map_order_iso_iff
modified theorem finset.sup_indep.bUnion
modified theorem finset.sup_indep.sup
modified theorem nhds_bot_basis
modified theorem nhds_bot_basis_Iic
modified theorem nhds_top_basis
modified theorem nhds_top_basis_Ici
added def sup.map
deleted def sup_top.map