id

Mathlib.Order.Hom.Lattice

URI: https://scilib.ai/kg/mathlib#LatticeHom.id

English

The identity map on a lattice is a lattice homomorphism.

Русский

Идентичный отображение на решетке является гомоморфизмом решетки.

LaTeX

$$$\mathrm{id}_{\alpha}: \alpha \to \alpha$ is a lattice homomorphism, i.e., preserves $\lor$ and $\land$.$$

Lean4

/-- `id` as a `LatticeHom`. -/
protected def id : LatticeHom α α where
  toFun := id
  map_sup' _ _ := rfl
  map_inf' _ _ := rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru