mem_cells

Mathlib.Combinatorics.Young.YoungDiagram

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

English

Membership in μ is equivalent to membership in μ.cells.

Русский

Принадлежность к μ эквивалентна принадлежности к μ.cells.

LaTeX

$$$\forall c:\; c\in μ.cells \iff c\in μ.$$$

Lean4

@[simp]
theorem mem_cells {μ : YoungDiagram} (c : ℕ × ℕ) : c ∈ μ.cells ↔ c ∈ μ :=
  Iff.rfl

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

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

Разделы

Аффилиация

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