∀ {α : 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 : Compl α] [inst_7 : HImp α] [inst_8 : SDiff α] [inst_9 : CompleteAtomicBooleanAlgebra β]
  (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_top : f ⊤ = ⊤)
  (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b)
  (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) (a b : α), Lattice.inf a b ≤ a