Theorem le_biSup

Modification history

2025-01-10 13:20

Mathlib/Order/CompleteLattice.lean

feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) …

Modified le_biSup View on Github →

2024-02-01 05:56

Mathlib/Order/CompleteLattice.lean

feat: a supremum of semisimple modules is semisimple (#10086) …

Added le_biSup View on Github →