Theorem Order.Ideal.top_of_top_mem

Modification history

2026-04-22 14:48

Mathlib/Order/Ideal.lean

feat(Order/Ideal): more results on order ideals (#34820) …

Deleted Order.Ideal.top_of_top_mem View on Github →

2023-02-02 09:51

Mathlib/Order/Ideal.lean

feat: port Order.Ideal (#1985)

Added Order.Ideal.top_of_top_mem View on Github →