id — Mathlib · SciLib

English

The identity map on any lattice α forms a bounded lattice homomorphism from α to α.

Русский

Идентичное отображение на решетке α образует гомоморфизм ограниченной решетки α → α.

LaTeX

$$$\\forall a\\in\\alpha:\\ (\\mathrm{BoundedLatticeHom.id}\,\\alpha)(a)=a$$$

Lean4

/-- `id` as a `BoundedLatticeHom`. -/
protected def id : BoundedLatticeHom α α :=
  { LatticeHom.id α, BoundedOrderHom.id α with }

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