Theorem not_mem_of_lt_csInf

Modification history

2025-05-25 12:30

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

chore(*): not_mem/nmem -> notMem (#25159)

Deleted not_mem_of_lt_csInf View on Github →

2023-05-14 07:05

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

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

Added not_mem_of_lt_csInf View on Github →