le_of_transpose_le

Mathlib.Combinatorics.Young.YoungDiagram

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

← MathLib Explorer

English

For μ, ν, μ.transpose ≤ ν.transpose iff μ ≤ ν.

Русский

Для диаграмм μ, ν выполняется μ.transpose ≤ ν.transpose тогда и только тогда μ ≤ ν.

LaTeX

$$$ μ.transpose \le ν.transpose \iff μ \le ν. $$$

Lean4

protected theorem le_of_transpose_le {μ ν : YoungDiagram} (h_le : μ.transpose ≤ ν) : μ ≤ ν.transpose := fun c hc =>
  by
  simp only [mem_cells, mem_transpose]
  apply h_le
  simpa

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

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

Разделы

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

Аффилиация

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