Theorem infiniteDimensionalOrder_of_strictMono

Modification history

2024-06-27 01:16
Mathlib/Order/RelSeries.lean
feat(Order/KrullDimension): add some basic lemmas about krull dimension of a preorder (#11147) …
Added infiniteDimensionalOrder_of_strictMonoView on Github →