colLen_anti

Mathlib.Combinatorics.Young.YoungDiagram

URI: https://scilib.ai/kg/mathlib#YoungDiagram.colLen_anti

← MathLib Explorer

English

If j1 ≤ j2, then μ.colLen(j2) ≤ μ.colLen(j1).

Русский

Если j1 ≤ j2, то μ.colLen(j2) ≤ μ.colLen(j1).

LaTeX

$$$$ \forall \mu, j_1, j_2 \,(j_1 \le j_2) \Rightarrow \mu.colLen(j_2) \le \mu.colLen(j_1). $$$$

Lean4

@[mono]
theorem colLen_anti (μ : YoungDiagram) (j1 j2 : ℕ) (hj : j1 ≤ j2) : μ.colLen j2 ≤ μ.colLen j1 := by
  convert μ.transpose.rowLen_anti j1 j2 hj using 1 <;> simp

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

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

Разделы

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

Аффилиация

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