Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-22 12:15 0e216ce0

View on Github →

feat(order): if s is finite then Sup s ∈ s (#7682)

Estimated changes

Modified src/order/conditionally_complete_lattice.lean

added theorem finset.nonempty.cInf_mem

added theorem finset.nonempty.cSup_mem

added theorem set.nonempty.cInf_mem

added theorem set.nonempty.cSup_mem