Commit 2026-02-16 16:43 1a11f9b0

View on Github →

feat: basic API for ConditionallyCompletePartialOrder (#35047) This develops the basic API for ConditionallyCompletePartialOrder. The API is copied from ConditionallyCompleteLattice, with DirectedOn assumptions added, and these lemmas are protected within that namespace. In a few cases, the lemmas were capable of being generalized outright, which we have done here. As a result, some material moved out of ConditionallyCompleteLattice/Basic to ConditionallyCompletePartialOrder/Basic.

Estimated changes

deleted theorem iInf_congr_Prop
deleted theorem iInf_of_isEmpty
deleted theorem sInf_image'
deleted theorem IsGreatest.csSup_eq
deleted theorem IsGreatest.csSup_mem
deleted theorem IsLeast.csInf_eq
deleted theorem IsLeast.csInf_mem
deleted theorem csInf_Icc
deleted theorem csInf_Ici
deleted theorem csInf_Ico
deleted theorem csInf_singleton
deleted theorem csSup_Icc
deleted theorem csSup_Iic
deleted theorem csSup_Ioc
deleted theorem csSup_singleton
deleted theorem inf_eq_bot_of_bot_mem
deleted theorem sup_eq_top_of_top_mem
deleted theorem cbiInf_eq_of_forall
deleted theorem cbiSup_eq_of_forall
deleted theorem ciInf_Ici
deleted theorem ciInf_const
deleted theorem ciInf_eq_ite
deleted theorem ciInf_neg
deleted theorem ciInf_pos
deleted theorem ciInf_subsingleton
deleted theorem ciInf_unique
deleted theorem ciSup_Iic
deleted theorem ciSup_const
deleted theorem ciSup_eq_ite
deleted theorem ciSup_neg
deleted theorem ciSup_pos
deleted theorem ciSup_subsingleton
deleted theorem ciSup_unique
added theorem IsGreatest.csSup_eq
added theorem IsGreatest.csSup_mem
added theorem IsGreatest.directedOn
added theorem csInf_Icc
added theorem csInf_Ici
added theorem csInf_Ico
added theorem csSup_Icc
added theorem csSup_Iic
added theorem csSup_Ioc
added theorem csSup_singleton
added theorem sup_eq_top_of_top_mem
added theorem Directed.Ici_ciSup
added theorem Directed.ciSup_le_iff
added theorem Directed.ciSup_mono
added theorem Directed.isLUB_ciSup
added theorem cbiSup_eq_of_forall
added theorem ciSup_Iic
added theorem ciSup_const
added theorem ciSup_eq_ite
added theorem ciSup_neg
added theorem ciSup_pos
added theorem ciSup_subsingleton
added theorem ciSup_unique