Theorem iInf_ne_of_notMem

Modification history

2026-09-03 15:14

Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

chore(Order/ConditionallyCompleteLattice/Finset): use `to_dual` (#43320) …

Deleted iInf_ne_of_notMem View on Github →

2026-06-13 13:42

Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

feat(Order/ConditionallyCompleteLattice/Finset): `sSup s ≠ ⊤` in a `CompleteLinearOrder` for a finite set without `⊤` (#38356) …

Added iInf_ne_of_notMem View on Github →