Commit 2023-09-22 18:39 d0f7245e

View on Github →

feat(Topology/Order): add IsClosed.isLeast_csInf (#7301) Also add IsClosed.isGreatest_csSup.

Estimated changes

Modified Mathlib/Topology/Order/Basic.lean

added theorem IsClosed.isGreatest_csSup

added theorem IsClosed.isLeast_csInf