∀ {α : Type u_1} {β : Type u_2} [inst : Max α] [inst_1 : Min α] [inst_2 : LE α] [inst_3 : LT α] [inst_4 : Top α]
  [inst_5 : Bot α] [inst_6 : SDiff α] [inst_7 : CoheytingAlgebra β] (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),
  f ⊤ = ⊤ → ∀ (map_bot : f ⊥ = ⊥) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) (a : α), a ≤ ⊤