Theorem WithTop.toDual_map

Modification history

2025-12-28 23:05

Mathlib/Order/WithBot.lean

chore(Order/WithBot): use `to_dual` (part 4) (#33267)

Deleted WithTop.toDual_map View on Github →

2022-11-29 20:56

Mathlib/Order/WithBot.lean

feat: port Order.WithBot (#777) …

Added WithTop.toDual_map View on Github →