Theorem IsCompact.exists_sSup_image_eq_and_ge

Modification history

2023-08-15 16:57

Mathlib/Topology/Algebra/Order/Compact.lean

feat: weaken assumptions for `IsCompact.existsIsLeast` and all of its variations (#6345) …

Modified IsCompact.exists_sSup_image_eq_and_ge View on Github →

2023-05-14 07:05

Mathlib/Topology/Algebra/Order/Compact.lean

chore: Rename to `sSup`/`iSup` (#3938) …

Added IsCompact.exists_sSup_image_eq_and_ge View on Github →