semilatticeSup — Mathlib

Lean4
/-- A type endowed with `⊔` is a `SemilatticeSup`, if it admits an injective map that
preserves `⊔` to a `SemilatticeSup`.
See note [reducible non-instances]. -/
protected abbrev semilatticeSup [Max α] [SemilatticeSup β] (f : α → β) (hf_inj : Function.Injective f)
    (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) : SemilatticeSup α
    where
  __ := PartialOrder.lift f hf_inj
  sup a b := max a b
  le_sup_left a
    b := by
    change f a ≤ f (a ⊔ b)
    rw [map_sup]
    exact le_sup_left
  le_sup_right a
    b := by
    change f b ≤ f (a ⊔ b)
    rw [map_sup]
    exact le_sup_right
  sup_le a b c ha
    hb := by
    change f (a ⊔ b) ≤ f c
    rw [map_sup]
    exact sup_le ha hb
Похожие утверждения