Commit 2025-05-02 21:42 58e0e1ca

feat: cofinal sets (#24290) A set s is dominated by a set t if for all a ∈ s there exists b ∈ t such that a ≤ b. This naturally occuring condition is equivalent to s ⊆ lowerClosure t, but it is difficult to prove things like transitivity from that definition alone. Better to have API. The import increase is immaterial.