Lean4
/-- A type endowed with `⊓` is a `SemilatticeInf`, if it admits an injective map that
preserves `⊓` to a `SemilatticeInf`.
See note [reducible non-instances]. -/
protected abbrev semilatticeInf [Min α] [SemilatticeInf β] (f : α → β) (hf_inj : Function.Injective f)
(map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) : SemilatticeInf α
where
__ := PartialOrder.lift f hf_inj
inf a b := min a b
inf_le_left a
b := by
change f (a ⊓ b) ≤ f a
rw [map_inf]
exact inf_le_left
inf_le_right a
b := by
change f (a ⊓ b) ≤ f b
rw [map_inf]
exact inf_le_right
le_inf a b c ha
hb := by
change f a ≤ f (b ⊓ c)
rw [map_inf]
exact le_inf ha hb