Revision #3452 → #3952 · back to history
modifiedAntisymmetric relation3b7e0848e670
| Field | From #3452 | To #3952 |
|---|
| mathlib.decl | IsAntisymm | Std.Antisymm |
| mathlib.module | Mathlib.Order.Defs.Unbundled | Init.Core |
| note | `IsAntisymm` is the typeclass encoding antisymmetry of a binary relation; underlies `PartialOrder`. | `Std.Antisymm r` is the core typeclass encoding antisymmetry `r a b → r b a → a = b` (the previously-cited `IsAntisymm` has been renamed). |
modifiedLimit ordinald84eadbefa67
| Field | From #3452 | To #3952 |
|---|
| mathlib.match_kind | exact | generalization |
| provenance | ai | ai-moderated |
modifiedSuccessor cardinal0aadee30f10d
| Field | From #3452 | To #3952 |
|---|
| mathlib.match_kind | exact | generalization |
| provenance | ai | ai-moderated |
addedUltrafilter lemma18d7e1f245c3
addedBoolean prime ideal theorem33c5fca06ea8
addedAlexander's subbase lemmac439627c147a
addedProper idealecbe12b1ba16
addedSpanning set239b6f8200c1
addedSuccessor ordinal04e1d15bc00e
addedBurali-Forti paradoxc5c470cc595e
addedℝ has a Hamel basis over ℚ84a26357c164