Commit 2025-02-17 21:24 ef5710b8

View on Github →

feat: generalize IsLUB.mem_of_not_isSuccPrelimit to LinearOrder (#20502)

Estimated changes

Modified Mathlib/Order/SuccPred/CompleteLinearOrder.lean

deleted theorem IsGLB.mem_of_not_isPredPrelimit

deleted theorem IsLUB.mem_of_not_isSuccPrelimit

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem IsGLB.isPredLimit_of_not_mem

added theorem IsGLB.isPredPrelimit_of_not_mem

added theorem IsGLB.mem_of_not_isPredLimit

added theorem IsGLB.mem_of_not_isPredPrelimit

added theorem IsLUB.isSuccLimit_of_not_mem

added theorem IsLUB.isSuccPrelimit_of_not_mem

added theorem IsLUB.mem_of_not_isSuccLimit

added theorem IsLUB.mem_of_not_isSuccPrelimit

Modified Mathlib/SetTheory/Cardinal/Basic.lean