∀ {α : Type u_1} {β : Type u_2} [inst : Min α] [inst_1 : LE α] [inst_2 : LT α] [inst_3 : SemilatticeInf β] (f : α → β)
  (hf_inj : Function.Injective f) (le : ∀ {y x : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {y x : α}, f x < f y ↔ x < y),
  (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) → ∀ (a b : α), a ⊓ b ≤ a