semilatticeInf — Mathlib

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
Похожие утверждения