ofHom — Mathlib

English

A bounded lattice homomorphism f: X → Y can be viewed as a morphism in FinBddDistLat from of X to of Y.

Русский

Гомоморфизм ограниченной решетки f: X → Y можно рассматривать как морфизм в FinBddDistLat между of X и of Y.

LaTeX

$$ofHom(f) : FinBddDistLat.of X ⟶ FinBddDistLat.of Y$$

Lean4

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

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