exists_notMem_col

Mathlib.Combinatorics.Young.YoungDiagram

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

← MathLib Explorer

English

For every μ and j, there exists i such that (i,j) is not in μ.cells.

Русский

Для каждой μ и j существует i такое, что (i,j) не принадлежит μ.cells.

LaTeX

$$$$ \exists i \in \mathbb{N}, (i,j) \notin \mu.cells. $$$$

Lean4

protected theorem exists_notMem_col (μ : YoungDiagram) (j : ℕ) : ∃ i, (i, j) ∉ μ.cells :=
  by
  convert μ.transpose.exists_notMem_row j using 1
  simp

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

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

Разделы

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

Аффилиация

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