ofHom — Mathlib

English

Typecheck a bounded lattice hom as a morphism in BddLat; i.e., a map that respects lattice operations and bounds can be regarded as a morphism in the category BddLat.

Русский

Любой гомоморфизм ограниченной решётки с сохранением операций и границ может рассматриваться как морфа в категории BddLat.

LaTeX

$$$ \mathrm{OfHom}(f) : \mathrm{of}(X) \to \mathrm{of}(Y) $$$

Lean4

/-- Typecheck a `BoundedLatticeHom` as a morphism in `BddLat`. -/
abbrev ofHom {X Y : Type u} [Lattice X] [BoundedOrder X] [Lattice Y] [BoundedOrder Y] (f : BoundedLatticeHom X Y) :
    of X ⟶ of Y :=
  ConcreteCategory.ofHom (C := BddLat) f

Похожие утверждения