Commit 2025-03-24 10:45 fb92bc76

View on Github →

chore: split Order.UpperLower.Basic (#23248) All of the replacement files are still in Order.UpperLower.

  • Basic now focuses on the unbundled predicates IsUpperSet and IsLowerSet.
  • CompleteLattice constructs the complete lattice instances on the bundled UpperSet and LowerSet.
  • Principal defines principal upper and lower sets (one element).
  • Closure defines upper and lower closures (arbitrary elements).
  • Prod defines the Cartesian product of upper or lower sets.
  • Fibration proves a few interactions between fibrations and upper/lower sets.

Estimated changes

deleted theorem IsLowerSet.prod
deleted theorem IsUpperSet.prod
deleted theorem LowerSet.Ici_prod_Ici
deleted theorem LowerSet.Iic_iInf
deleted theorem LowerSet.Iic_iInf₂
deleted theorem LowerSet.Iic_inf
deleted theorem LowerSet.Iic_inj
deleted theorem LowerSet.Iic_le
deleted theorem LowerSet.Iic_ne_Iic
deleted theorem LowerSet.Iic_ne_bot
deleted theorem LowerSet.Iic_prod
deleted theorem LowerSet.Iic_sInf
deleted theorem LowerSet.Iic_sup_erase
deleted theorem LowerSet.Ioi_le_Ici
deleted def LowerSet.Simps.coe
deleted theorem LowerSet.bot_lt_Iic
deleted theorem LowerSet.bot_prod
deleted theorem LowerSet.carrier_eq_coe
deleted theorem LowerSet.coe_Iic
deleted theorem LowerSet.coe_Iio
deleted theorem LowerSet.coe_bot
deleted theorem LowerSet.coe_compl
deleted theorem LowerSet.coe_eq_empty
deleted theorem LowerSet.coe_eq_univ
deleted theorem LowerSet.coe_erase
deleted theorem LowerSet.coe_iInf
deleted theorem LowerSet.coe_iInf₂
deleted theorem LowerSet.coe_iSup
deleted theorem LowerSet.coe_iSup₂
deleted theorem LowerSet.coe_inf
deleted theorem LowerSet.coe_map
deleted theorem LowerSet.coe_mk
deleted theorem LowerSet.coe_nonempty
deleted theorem LowerSet.coe_prod
deleted theorem LowerSet.coe_sInf
deleted theorem LowerSet.coe_sSup
deleted theorem LowerSet.coe_sdiff
deleted theorem LowerSet.coe_ssubset_coe
deleted theorem LowerSet.coe_subset_coe
deleted theorem LowerSet.coe_sup
deleted theorem LowerSet.coe_top
deleted def LowerSet.compl
deleted theorem LowerSet.compl_iInf₂
deleted theorem LowerSet.compl_iSup₂
deleted theorem LowerSet.compl_le_compl
deleted theorem LowerSet.compl_map
deleted theorem LowerSet.disjoint_coe
deleted theorem LowerSet.disjoint_prod
deleted def LowerSet.erase
deleted theorem LowerSet.erase_eq
deleted theorem LowerSet.erase_idem
deleted theorem LowerSet.erase_le
deleted theorem LowerSet.erase_lt
deleted theorem LowerSet.erase_sup_Iic
deleted theorem LowerSet.ext
deleted theorem LowerSet.iSup_Iic
deleted theorem LowerSet.inf_prod
deleted def LowerSet.map
deleted theorem LowerSet.map_Iic
deleted theorem LowerSet.map_Iio
deleted theorem LowerSet.map_map
deleted theorem LowerSet.map_refl
deleted theorem LowerSet.mem_Iic_iff
deleted theorem LowerSet.mem_Iio_iff
deleted theorem LowerSet.mem_compl_iff
deleted theorem LowerSet.mem_iInf_iff
deleted theorem LowerSet.mem_iInf₂_iff
deleted theorem LowerSet.mem_iSup_iff
deleted theorem LowerSet.mem_iSup₂_iff
deleted theorem LowerSet.mem_inf_iff
deleted theorem LowerSet.mem_map
deleted theorem LowerSet.mem_mk
deleted theorem LowerSet.mem_prod
deleted theorem LowerSet.mem_sInf_iff
deleted theorem LowerSet.mem_sSup_iff
deleted theorem LowerSet.mem_sup_iff
deleted theorem LowerSet.mem_top
deleted theorem LowerSet.not_mem_bot
deleted def LowerSet.prod
deleted theorem LowerSet.prod_bot
deleted theorem LowerSet.prod_eq_bot
deleted theorem LowerSet.prod_inf
deleted theorem LowerSet.prod_inf_prod
deleted theorem LowerSet.prod_le_prod_iff
deleted theorem LowerSet.prod_mono
deleted theorem LowerSet.prod_mono_left
deleted theorem LowerSet.prod_mono_right
deleted theorem LowerSet.prod_sup
deleted def LowerSet.sdiff
deleted theorem LowerSet.sdiff_le_left
deleted theorem LowerSet.sdiff_lt_left
deleted theorem LowerSet.sdiff_singleton
deleted theorem LowerSet.sup_prod
deleted theorem LowerSet.symm_map
deleted theorem LowerSet.top_prod_top
deleted theorem UpperSet.Ici_iSup
deleted theorem UpperSet.Ici_iSup₂
deleted theorem UpperSet.Ici_inf_erase
deleted theorem UpperSet.Ici_inj
deleted theorem UpperSet.Ici_le_Ioi
deleted theorem UpperSet.Ici_lt_top
deleted theorem UpperSet.Ici_ne_Ici
deleted theorem UpperSet.Ici_ne_top
deleted theorem UpperSet.Ici_prod
deleted theorem UpperSet.Ici_prod_Ici
deleted theorem UpperSet.Ici_sSup
deleted theorem UpperSet.Ici_sup
deleted def UpperSet.Simps.coe
deleted theorem UpperSet.bot_prod_bot
deleted theorem UpperSet.carrier_eq_coe
deleted theorem UpperSet.codisjoint_coe
deleted theorem UpperSet.codisjoint_prod
deleted theorem UpperSet.coe_Ici
deleted theorem UpperSet.coe_Ioi
deleted theorem UpperSet.coe_bot
deleted theorem UpperSet.coe_compl
deleted theorem UpperSet.coe_eq_empty
deleted theorem UpperSet.coe_eq_univ
deleted theorem UpperSet.coe_erase
deleted theorem UpperSet.coe_iInf
deleted theorem UpperSet.coe_iInf₂
deleted theorem UpperSet.coe_iSup
deleted theorem UpperSet.coe_iSup₂
deleted theorem UpperSet.coe_inf
deleted theorem UpperSet.coe_map
deleted theorem UpperSet.coe_mk
deleted theorem UpperSet.coe_nonempty
deleted theorem UpperSet.coe_prod
deleted theorem UpperSet.coe_sInf
deleted theorem UpperSet.coe_sSup
deleted theorem UpperSet.coe_sdiff
deleted theorem UpperSet.coe_ssubset_coe
deleted theorem UpperSet.coe_subset_coe
deleted theorem UpperSet.coe_sup
deleted theorem UpperSet.coe_top
deleted def UpperSet.compl
deleted theorem UpperSet.compl_iInf₂
deleted theorem UpperSet.compl_iSup₂
deleted theorem UpperSet.compl_le_compl
deleted theorem UpperSet.compl_map
deleted def UpperSet.erase
deleted theorem UpperSet.erase_eq
deleted theorem UpperSet.erase_idem
deleted theorem UpperSet.erase_inf_Ici
deleted theorem UpperSet.ext
deleted theorem UpperSet.iInf_Ici
deleted theorem UpperSet.inf_prod
deleted theorem UpperSet.le_Ici
deleted theorem UpperSet.le_erase
deleted theorem UpperSet.le_sdiff_left
deleted theorem UpperSet.lt_erase
deleted theorem UpperSet.lt_sdiff_left
deleted def UpperSet.map
deleted theorem UpperSet.map_Ici
deleted theorem UpperSet.map_Ioi
deleted theorem UpperSet.map_map
deleted theorem UpperSet.map_refl
deleted theorem UpperSet.mem_Ici_iff
deleted theorem UpperSet.mem_Ioi_iff
deleted theorem UpperSet.mem_bot
deleted theorem UpperSet.mem_compl_iff
deleted theorem UpperSet.mem_iInf_iff
deleted theorem UpperSet.mem_iInf₂_iff
deleted theorem UpperSet.mem_iSup_iff
deleted theorem UpperSet.mem_iSup₂_iff
deleted theorem UpperSet.mem_inf_iff
deleted theorem UpperSet.mem_map
deleted theorem UpperSet.mem_mk
deleted theorem UpperSet.mem_prod
deleted theorem UpperSet.mem_sInf_iff
deleted theorem UpperSet.mem_sSup_iff
deleted theorem UpperSet.mem_sup_iff
deleted theorem UpperSet.not_mem_top
deleted def UpperSet.prod
deleted theorem UpperSet.prod_eq_top
deleted theorem UpperSet.prod_inf
deleted theorem UpperSet.prod_le_prod_iff
deleted theorem UpperSet.prod_mono
deleted theorem UpperSet.prod_mono_left
deleted theorem UpperSet.prod_mono_right
deleted theorem UpperSet.prod_sup
deleted theorem UpperSet.prod_sup_prod
deleted theorem UpperSet.prod_top
deleted def UpperSet.sdiff
deleted theorem UpperSet.sdiff_singleton
deleted theorem UpperSet.sup_prod
deleted theorem UpperSet.symm_map
deleted theorem UpperSet.top_prod
deleted theorem bddAbove_lowerClosure
deleted theorem bddBelow_upperClosure
deleted theorem coe_lowerClosure
deleted theorem coe_upperClosure
deleted theorem gc_lowerClosure_coe
deleted theorem gc_upperClosure_coe
deleted def giLowerClosureCoe
deleted def giUpperClosureCoe
deleted theorem le_upperClosure
deleted theorem lowerBounds_upperClosure
deleted def lowerClosure
deleted theorem lowerClosure_empty
deleted theorem lowerClosure_eq
deleted theorem lowerClosure_eq_bot_iff
deleted theorem lowerClosure_iUnion
deleted theorem lowerClosure_image
deleted theorem lowerClosure_le
deleted theorem lowerClosure_min
deleted theorem lowerClosure_mono
deleted theorem lowerClosure_prod
deleted theorem lowerClosure_sUnion
deleted theorem lowerClosure_singleton
deleted theorem lowerClosure_union
deleted theorem lowerClosure_univ
deleted theorem mem_lowerClosure
deleted theorem mem_upperClosure
deleted theorem subset_lowerClosure
deleted theorem subset_upperClosure
deleted theorem upperBounds_lowerClosure
deleted def upperClosure
deleted theorem upperClosure_anti
deleted theorem upperClosure_empty
deleted theorem upperClosure_eq
deleted theorem upperClosure_eq_top_iff
deleted theorem upperClosure_iUnion
deleted theorem upperClosure_image
deleted theorem upperClosure_min
deleted theorem upperClosure_prod
deleted theorem upperClosure_sUnion
deleted theorem upperClosure_singleton
deleted theorem upperClosure_union
deleted theorem upperClosure_univ
deleted def upperSetIsoLowerSet
added theorem LowerSet.Iic_sup_erase
added theorem LowerSet.coe_erase
added theorem LowerSet.coe_sdiff
added def LowerSet.erase
added theorem LowerSet.erase_eq
added theorem LowerSet.erase_idem
added theorem LowerSet.erase_le
added theorem LowerSet.erase_lt
added theorem LowerSet.erase_sup_Iic
added theorem LowerSet.iSup_Iic
added def LowerSet.sdiff
added theorem LowerSet.sdiff_le_left
added theorem LowerSet.sdiff_lt_left
added theorem UpperSet.Ici_inf_erase
added theorem UpperSet.coe_erase
added theorem UpperSet.coe_sdiff
added def UpperSet.erase
added theorem UpperSet.erase_eq
added theorem UpperSet.erase_idem
added theorem UpperSet.erase_inf_Ici
added theorem UpperSet.iInf_Ici
added theorem UpperSet.le_erase
added theorem UpperSet.le_sdiff_left
added theorem UpperSet.lt_erase
added theorem UpperSet.lt_sdiff_left
added def UpperSet.sdiff
added theorem bddAbove_lowerClosure
added theorem bddBelow_upperClosure
added theorem coe_lowerClosure
added theorem coe_upperClosure
added theorem gc_lowerClosure_coe
added theorem gc_upperClosure_coe
added theorem le_upperClosure
added def lowerClosure
added theorem lowerClosure_empty
added theorem lowerClosure_eq
added theorem lowerClosure_iUnion
added theorem lowerClosure_image
added theorem lowerClosure_le
added theorem lowerClosure_min
added theorem lowerClosure_mono
added theorem lowerClosure_sUnion
added theorem lowerClosure_singleton
added theorem lowerClosure_union
added theorem lowerClosure_univ
added theorem mem_lowerClosure
added theorem mem_upperClosure
added theorem subset_lowerClosure
added theorem subset_upperClosure
added def upperClosure
added theorem upperClosure_anti
added theorem upperClosure_empty
added theorem upperClosure_eq
added theorem upperClosure_iUnion
added theorem upperClosure_image
added theorem upperClosure_min
added theorem upperClosure_sUnion
added theorem upperClosure_singleton
added theorem upperClosure_union
added theorem upperClosure_univ
added theorem LowerSet.coe_bot
added theorem LowerSet.coe_compl
added theorem LowerSet.coe_eq_empty
added theorem LowerSet.coe_eq_univ
added theorem LowerSet.coe_iInf
added theorem LowerSet.coe_iInf₂
added theorem LowerSet.coe_iSup
added theorem LowerSet.coe_iSup₂
added theorem LowerSet.coe_inf
added theorem LowerSet.coe_map
added theorem LowerSet.coe_mk
added theorem LowerSet.coe_nonempty
added theorem LowerSet.coe_sInf
added theorem LowerSet.coe_sSup
added theorem LowerSet.coe_sup
added theorem LowerSet.coe_top
added def LowerSet.compl
added theorem LowerSet.compl_iInf₂
added theorem LowerSet.compl_iSup₂
added theorem LowerSet.compl_map
added theorem LowerSet.disjoint_coe
added theorem LowerSet.ext
added def LowerSet.map
added theorem LowerSet.map_map
added theorem LowerSet.map_refl
added theorem LowerSet.mem_compl_iff
added theorem LowerSet.mem_iInf_iff
added theorem LowerSet.mem_iSup_iff
added theorem LowerSet.mem_inf_iff
added theorem LowerSet.mem_map
added theorem LowerSet.mem_mk
added theorem LowerSet.mem_sInf_iff
added theorem LowerSet.mem_sSup_iff
added theorem LowerSet.mem_sup_iff
added theorem LowerSet.mem_top
added theorem LowerSet.not_mem_bot
added theorem LowerSet.symm_map
added theorem UpperSet.coe_bot
added theorem UpperSet.coe_compl
added theorem UpperSet.coe_eq_empty
added theorem UpperSet.coe_eq_univ
added theorem UpperSet.coe_iInf
added theorem UpperSet.coe_iInf₂
added theorem UpperSet.coe_iSup
added theorem UpperSet.coe_iSup₂
added theorem UpperSet.coe_inf
added theorem UpperSet.coe_map
added theorem UpperSet.coe_mk
added theorem UpperSet.coe_nonempty
added theorem UpperSet.coe_sInf
added theorem UpperSet.coe_sSup
added theorem UpperSet.coe_sup
added theorem UpperSet.coe_top
added def UpperSet.compl
added theorem UpperSet.compl_iInf₂
added theorem UpperSet.compl_iSup₂
added theorem UpperSet.compl_map
added theorem UpperSet.ext
added def UpperSet.map
added theorem UpperSet.map_map
added theorem UpperSet.map_refl
added theorem UpperSet.mem_bot
added theorem UpperSet.mem_compl_iff
added theorem UpperSet.mem_iInf_iff
added theorem UpperSet.mem_iSup_iff
added theorem UpperSet.mem_inf_iff
added theorem UpperSet.mem_map
added theorem UpperSet.mem_mk
added theorem UpperSet.mem_sInf_iff
added theorem UpperSet.mem_sSup_iff
added theorem UpperSet.mem_sup_iff
added theorem UpperSet.not_mem_top
added theorem UpperSet.symm_map
added theorem LowerSet.Iic_iInf
added theorem LowerSet.Iic_iInf₂
added theorem LowerSet.Iic_inf
added theorem LowerSet.Iic_inj
added theorem LowerSet.Iic_le
added theorem LowerSet.Iic_ne_Iic
added theorem LowerSet.Iic_ne_bot
added theorem LowerSet.Iic_sInf
added theorem LowerSet.Ioi_le_Ici
added theorem LowerSet.bot_lt_Iic
added theorem LowerSet.coe_Iic
added theorem LowerSet.coe_Iio
added theorem LowerSet.map_Iic
added theorem LowerSet.map_Iio
added theorem LowerSet.mem_Iic_iff
added theorem LowerSet.mem_Iio_iff
added theorem UpperSet.Ici_iSup
added theorem UpperSet.Ici_iSup₂
added theorem UpperSet.Ici_inj
added theorem UpperSet.Ici_le_Ioi
added theorem UpperSet.Ici_lt_top
added theorem UpperSet.Ici_ne_Ici
added theorem UpperSet.Ici_ne_top
added theorem UpperSet.Ici_sSup
added theorem UpperSet.Ici_sup
added theorem UpperSet.coe_Ici
added theorem UpperSet.coe_Ioi
added theorem UpperSet.le_Ici
added theorem UpperSet.map_Ici
added theorem UpperSet.map_Ioi
added theorem UpperSet.mem_Ici_iff
added theorem UpperSet.mem_Ioi_iff
added theorem IsLowerSet.prod
added theorem IsUpperSet.prod
added theorem LowerSet.Ici_prod_Ici
added theorem LowerSet.Iic_prod
added theorem LowerSet.bot_prod
added theorem LowerSet.coe_prod
added theorem LowerSet.disjoint_prod
added theorem LowerSet.inf_prod
added theorem LowerSet.mem_prod
added def LowerSet.prod
added theorem LowerSet.prod_bot
added theorem LowerSet.prod_eq_bot
added theorem LowerSet.prod_inf
added theorem LowerSet.prod_inf_prod
added theorem LowerSet.prod_mono
added theorem LowerSet.prod_sup
added theorem LowerSet.sup_prod
added theorem LowerSet.top_prod_top
added theorem UpperSet.Ici_prod
added theorem UpperSet.Ici_prod_Ici
added theorem UpperSet.bot_prod_bot
added theorem UpperSet.coe_prod
added theorem UpperSet.inf_prod
added theorem UpperSet.mem_prod
added def UpperSet.prod
added theorem UpperSet.prod_eq_top
added theorem UpperSet.prod_inf
added theorem UpperSet.prod_mono
added theorem UpperSet.prod_sup
added theorem UpperSet.prod_sup_prod
added theorem UpperSet.prod_top
added theorem UpperSet.sup_prod
added theorem UpperSet.top_prod
added theorem lowerClosure_prod
added theorem upperClosure_prod