coe_inf

Mathlib.Combinatorics.Young.YoungDiagram

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

English

The set of cells of μ ⊓ ν equals μ.cells ∩ ν.cells.

Русский

Множество клеток μ ⊓ ν равно μ.cells ∩ ν.cells.

LaTeX

$$$ (μ ⊓ ν).cells = μ.cells \cap ν.cells. $$$

Lean4

@[simp, norm_cast]
theorem coe_inf (μ ν : YoungDiagram) : ↑(μ ⊓ ν) = (μ ∩ ν : Set (ℕ × ℕ)) :=
  Finset.coe_inter _ _

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

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

Разделы

Аффилиация

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