Theorem OrderIso.isGLB_image'

Modification history

2026-09-07 15:38
Mathlib/Order/Bounds/OrderIso.lean
chore(Order): use `to_dual` in various places (#43323) …
Deleted OrderIso.isGLB_image'View on Github →
2022-12-16 03:25
Mathlib/Order/Bounds/OrderIso.lean
feat: port Order.Bounds.OrderIso (#1063) …
Added OrderIso.isGLB_image'View on Github →