boundary_zero

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#CompositionAsSet.boundary_zero

← MathLib Explorer

English

The image of the first boundary under boundary is 0.

Русский

Изображение нулевого элемента границ под boundary равно 0.

LaTeX

$$boundary(0) = 0$$

Lean4

@[simp]
theorem boundary_zero : (c.boundary ⟨0, c.card_boundaries_pos⟩ : Fin (n + 1)) = 0 :=
  by
  rw [boundary, Finset.orderEmbOfFin_zero rfl c.card_boundaries_pos]
  exact le_antisymm (Finset.min'_le _ _ c.zero_mem) (Fin.zero_le _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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