Commit 2024-10-22 14:55 f8c840f2

View on Github →

refactor(Order/ConditionallyCompleteLattice): split large file (#18029)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Group/CompleteLattice.lean

Modified Mathlib/Algebra/Order/Group/Indicator.lean

Modified Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean

Modified Mathlib/Data/Real/Archimedean.lean

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

deleted theorem GaloisConnection.l_ciSup

deleted theorem GaloisConnection.l_ciSup_set

deleted theorem GaloisConnection.l_csSup'

deleted theorem GaloisConnection.l_csSup

deleted theorem GaloisConnection.u_ciInf

deleted theorem GaloisConnection.u_ciInf_set

deleted theorem GaloisConnection.u_csInf'

deleted theorem GaloisConnection.u_csInf

deleted theorem IsGLB.ciInf_eq

deleted theorem IsGLB.ciInf_set_eq

deleted theorem IsLUB.ciSup_eq

deleted theorem IsLUB.ciSup_set_eq

deleted theorem Monotone.ciSup_mem_iInter_Icc_of_antitone

deleted theorem OrderIso.map_ciInf

deleted theorem OrderIso.map_ciInf_set

deleted theorem OrderIso.map_ciSup

deleted theorem OrderIso.map_ciSup_set

deleted theorem OrderIso.map_csInf'

deleted theorem OrderIso.map_csInf

deleted theorem OrderIso.map_csSup'

deleted theorem OrderIso.map_csSup

deleted theorem Set.Ici_ciSup

deleted theorem Set.Iic_ciInf

deleted theorem WithBot.ciSup_empty

deleted theorem WithBot.coe_iInf

deleted theorem WithBot.coe_iSup

deleted theorem WithTop.coe_iInf

deleted theorem WithTop.coe_iSup

deleted theorem WithTop.iInf_coe_eq_top

deleted theorem WithTop.iInf_coe_lt_top

deleted theorem WithTop.iInf_empty

deleted theorem WithTop.iSup_coe_eq_top

deleted theorem WithTop.iSup_coe_lt_top

deleted theorem cbiInf_eq_of_forall

deleted theorem cbiInf_eq_of_not_forall

deleted theorem cbiSup_eq_of_forall

deleted theorem cbiSup_eq_of_not_forall

deleted theorem ciInf_const

deleted theorem ciInf_eq_bot_of_bot_mem

deleted theorem ciInf_eq_ite

deleted theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt

deleted theorem ciInf_eq_top_of_top_mem

deleted theorem ciInf_image

deleted theorem ciInf_le'

deleted theorem ciInf_le

deleted theorem ciInf_le_of_le'

deleted theorem ciInf_le_of_le

deleted theorem ciInf_lt_iff

deleted theorem ciInf_mem

deleted theorem ciInf_mono

deleted theorem ciInf_neg

deleted theorem ciInf_pos

deleted theorem ciInf_set_le

deleted theorem ciInf_subsingleton

deleted theorem ciInf_subtype''

deleted theorem ciInf_subtype'

deleted theorem ciInf_subtype

deleted theorem ciInf_unique

deleted theorem ciSup_const

deleted theorem ciSup_eq_ite

deleted theorem ciSup_eq_of_forall_le_of_forall_lt_exists_gt

deleted theorem ciSup_false

deleted theorem ciSup_image

deleted theorem ciSup_le'

deleted theorem ciSup_le

deleted theorem ciSup_le_iff'

deleted theorem ciSup_le_iff

deleted theorem ciSup_mem_iInter_Icc_of_antitone_Icc

deleted theorem ciSup_mono'

deleted theorem ciSup_mono

deleted theorem ciSup_neg

deleted theorem ciSup_of_empty

deleted theorem ciSup_or'

deleted theorem ciSup_pos

deleted theorem ciSup_set_le_iff

deleted theorem ciSup_subsingleton

deleted theorem ciSup_subtype''

deleted theorem ciSup_subtype'

deleted theorem ciSup_subtype

deleted theorem ciSup_unique

deleted theorem csInf_image

deleted theorem csSup_image

deleted theorem exists_lt_of_ciInf_lt

deleted theorem exists_lt_of_lt_ciSup'

deleted theorem exists_lt_of_lt_ciSup

deleted theorem isGLB_ciInf

deleted theorem isGLB_ciInf_set

deleted theorem isLUB_ciSup

deleted theorem isLUB_ciSup_set

deleted theorem le_ciInf

deleted theorem le_ciInf_iff'

deleted theorem le_ciInf_iff

deleted theorem le_ciInf_set_iff

deleted theorem le_ciSup

deleted theorem le_ciSup_iff'

deleted theorem le_ciSup_of_le

deleted theorem le_ciSup_set

deleted theorem lt_ciSup_iff'

deleted theorem lt_ciSup_iff

Modified Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Group.lean

Created Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

added theorem GaloisConnection.l_ciSup

added theorem GaloisConnection.l_ciSup_set

added theorem GaloisConnection.l_csSup'

added theorem GaloisConnection.l_csSup

added theorem GaloisConnection.u_ciInf

added theorem GaloisConnection.u_ciInf_set

added theorem GaloisConnection.u_csInf'

added theorem GaloisConnection.u_csInf

added theorem IsGLB.ciInf_eq

added theorem IsGLB.ciInf_set_eq

added theorem IsLUB.ciSup_eq

added theorem IsLUB.ciSup_set_eq

added theorem Monotone.ciSup_mem_iInter_Icc_of_antitone

added theorem OrderIso.map_ciInf

added theorem OrderIso.map_ciInf_set

added theorem OrderIso.map_ciSup

added theorem OrderIso.map_ciSup_set

added theorem OrderIso.map_csInf'

added theorem OrderIso.map_csInf

added theorem OrderIso.map_csSup'

added theorem OrderIso.map_csSup

added theorem Set.Ici_ciSup

added theorem Set.Iic_ciInf

added theorem WithBot.ciSup_empty

added theorem WithBot.coe_iInf

added theorem WithBot.coe_iSup

added theorem WithTop.coe_iInf

added theorem WithTop.coe_iSup

added theorem WithTop.iInf_coe_eq_top

added theorem WithTop.iInf_coe_lt_top

added theorem WithTop.iInf_empty

added theorem WithTop.iSup_coe_eq_top

added theorem WithTop.iSup_coe_lt_top

added theorem cbiInf_eq_of_forall

added theorem cbiInf_eq_of_not_forall

added theorem cbiSup_eq_of_forall

added theorem cbiSup_eq_of_not_forall

added theorem ciInf_const

added theorem ciInf_eq_bot_of_bot_mem

added theorem ciInf_eq_ite

added theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt

added theorem ciInf_eq_top_of_top_mem

added theorem ciInf_image

added theorem ciInf_le'

added theorem ciInf_le

added theorem ciInf_le_of_le'

added theorem ciInf_le_of_le

added theorem ciInf_lt_iff

added theorem ciInf_mem

added theorem ciInf_mono

added theorem ciInf_neg

added theorem ciInf_pos

added theorem ciInf_set_le

added theorem ciInf_subsingleton

added theorem ciInf_subtype''

added theorem ciInf_subtype'

added theorem ciInf_subtype

added theorem ciInf_unique

added theorem ciSup_const

added theorem ciSup_eq_ite

added theorem ciSup_eq_of_forall_le_of_forall_lt_exists_gt

added theorem ciSup_false

added theorem ciSup_image

added theorem ciSup_le'

added theorem ciSup_le

added theorem ciSup_le_iff'

added theorem ciSup_le_iff

added theorem ciSup_mem_iInter_Icc_of_antitone_Icc

added theorem ciSup_mono'

added theorem ciSup_mono

added theorem ciSup_neg

added theorem ciSup_of_empty

added theorem ciSup_or'

added theorem ciSup_pos

added theorem ciSup_set_le_iff

added theorem ciSup_subsingleton

added theorem ciSup_subtype''

added theorem ciSup_subtype'

added theorem ciSup_subtype

added theorem ciSup_unique

added theorem csInf_image

added theorem csSup_image

added theorem exists_lt_of_ciInf_lt

added theorem exists_lt_of_lt_ciSup'

added theorem exists_lt_of_lt_ciSup

added theorem isGLB_ciInf

added theorem isGLB_ciInf_set

added theorem isLUB_ciSup

added theorem isLUB_ciSup_set

added theorem le_ciInf

added theorem le_ciInf_iff'

added theorem le_ciInf_iff

added theorem le_ciInf_set_iff

added theorem le_ciSup

added theorem le_ciSup_iff'

added theorem le_ciSup_of_le

added theorem le_ciSup_set

added theorem lt_ciSup_iff'

added theorem lt_ciSup_iff

Modified Mathlib/Order/Filter/AtTopBot.lean

Modified Mathlib/Order/Filter/Extr.lean

Modified Mathlib/Order/PartialSups.lean

Modified Mathlib/Order/SemiconjSup.lean

Modified Mathlib/Order/SuccPred/CompleteLinearOrder.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean