Def LocallyFiniteOrderTop.ofIic

Modification history

2024-03-18 10:51

Mathlib/Order/LocallyFinite.lean

fix: rename `LocallyFiniteOrderTop.ofIic` to `LocallyFiniteOrderBot` (#11371) …

Deleted LocallyFiniteOrderTop.ofIic View on Github →

2023-08-10 19:52

Mathlib/Order/LocallyFinite.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified LocallyFiniteOrderTop.ofIic View on Github →

2023-01-26 07:43

Mathlib/Order/LocallyFinite.lean

feat: port Order.LocallyFinite (#1754)

Added LocallyFiniteOrderTop.ofIic View on Github →