Theorem IsCompact.sSup_lt_iff_of_continuous

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.sSup_lt_iff_of_continuous View on Github →

2023-05-14 07:05

Mathlib/Topology/Algebra/Order/Compact.lean

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

Added IsCompact.sSup_lt_iff_of_continuous View on Github →