Theorem WithBot.ofDual_symm_apply

Modification history

2026-07-15 16:59
Mathlib/Order/WithBot.lean
chore: delete deprecated declarations to the end of 2025 (#41178) …
Deleted WithBot.ofDual_symm_applyView on Github →
2025-12-28 23:05
Mathlib/Order/WithBot.lean
chore(Order/WithBot): use `to_dual` (part 4) (#33267)
Modified WithBot.ofDual_symm_applyView on Github →
2025-02-12 11:53
Mathlib/Order/WithBot.lean
chore(Order/WithBot): golf, clean up (#21274) …
Modified WithBot.ofDual_symm_applyView on Github →
2022-11-29 20:56
Mathlib/Order/WithBot.lean
feat: port Order.WithBot (#777) …
Added WithBot.ofDual_symm_applyView on Github →