LeanPool.BruhatTits.Utils.Order

theorem OrderIso.map_top_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : α ≃o β) [OrderTop α] [OrderTop β] (x : α) : f x = ⊤ ↔ x = ⊤

theorem OrderIso.map_bot_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : α ≃o β) [OrderBot α] [OrderBot β] (x : α) : f x = ⊥ ↔ x = ⊥