Revision #2273 → #2665 · back to history
modifiedOrder on empty setb6c56bef23c0
| Field | From #2273 | To #2665 |
|---|
| mathlib.decl | Empty.instLinearOrder | instLinearOrderEmpty |
| provenance | ai | ai-moderated |
modifiedAlphabet dictionary orderbe5e72141563
| Field | From #2273 | To #2665 |
|---|
| mathlib.decl | Fintype.to_wellFoundedLT | Finite.to_wellFoundedLT |
| provenance | ai | ai-moderated |
modifiedFinite total order is a well ordera1702114b608
| Field | From #2273 | To #2665 |
|---|
| mathlib.decl | Fintype.to_wellFoundedLT | Finite.to_wellFoundedLT |
| provenance | ai | ai-moderated |
modifiedCompleteness iff closed bounded sets compactacc0722f129e
| Field | From #2273 | To #2665 |
|---|
| mathlib.decl | isCompact_Icc | CompactIccSpace.isCompact_Icc |
| provenance | ai | ai-moderated |
modifiedReal function defines strict weak order997fa1d7ab7e
| Field | From #2273 | To #2665 |
|---|
| mathlib.decl | instIsStrictWeakOrder | Order.Preimage.instIsStrictWeakOrder |
| provenance | ai | ai-moderated |