Commit 2025-07-14 14:29 94d81ee4

refactor: deprecate sSup_le_sSup_of_forall_exists_le in CompleteLattice in favor of sSup_le_sSup_of_isCofinalFor (#27124) The argument (h : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) of sSup_le_sSup_of_forall_exists_le is essentially IsCofinalFor s t, this PR therefore deprecates this theorem in favor of theorem sSup_le_sSup_of_isCofinalFor (h : IsCofinalFor s t) : sSup s ≤ sSup t. The same applies to sInf_le_sInf_of_forall_exists_le which is deprecated in favor of sInf_le_sInf_of_isCoinitialFor. TODO:

• When the tests pass, uncomment sSup_le_sSup_of_forall_exists_le and sInf_le_sInf_of_forall_exists_le and deprecate them.