∀ {α : Type u_1} {β : Type u_2} [inst : Max α] [inst_1 : Min α] [inst_2 : LE α] [inst_3 : LT α] [inst_4 : SupSet α]
  [inst_5 : InfSet α] [inst_6 : Top α] [inst_7 : Bot α] (minAx : Order.Coframe.MinimalAxioms β) (f : α → β)
  (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y)
  (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b)
  (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a)
  (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (a : α) (s : Set α), ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s