inl_bot

Mathlib.Data.Sum.Order

URI: https://scilib.ai/kg/mathlib#Sum.Lex.inl_bot

English

The toLex image of the bottom element in the left component equals the bottom of the Lex sum.

Русский

Изображение bottom слева равно нижнему элементу лексикографической суммы.

LaTeX

$$$\\text{toLex}(\\text{inl} \\bot) = \\bot$$$

Lean4

@[simp]
theorem inl_bot [LE α] [OrderBot α] [LE β] : toLex (inl ⊥ : α ⊕ β) = ⊥ :=
  rfl

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

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

Разделы

Аффилиация

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