liftLatticeHom_injective

Mathlib.Order.Booleanisation

URI: https://scilib.ai/kg/mathlib#Booleanisation.liftLatticeHom_injective

English

The embedding liftLatticeHom (α) into Booleanisation α is injective.

Русский

Встраивание liftLatticeHom (α) в Booleanisation α инъективно.

LaTeX

$$Injective( liftLatticeHom(α) )$$

Lean4

theorem liftLatticeHom_injective : Injective (liftLatticeHom (α := α)) :=
  Sum.inl_injective

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

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

Разделы

Аффилиация

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