birkhoffFinset_injective

Mathlib.Order.Birkhoff

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

English

The embedding birkhoffFinset is injective.

Русский

Вложение birkhoffFinset инъективно.

LaTeX

$$$\\operatorname{Injective}(\\operatorname{birkhoffFinset}(\\alpha := α))$$$

Lean4

theorem birkhoffFinset_injective : Injective (birkhoffFinset (α := α)) :=
  OrderEmbedding.birkhoffFinset.injective

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

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

Разделы

Аффилиация

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