mem_mk

Mathlib.Combinatorics.Young.YoungDiagram

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

English

Same as mem_mk: a point belongs to μ iff it belongs to μ.cells.

Русский

Как и mem_mk: точка принадлежит μ тогда и только тогда, когда она принадлежит μ.cells.

LaTeX

$$$c\in μ.cells \iff c\in μ.$$$

Lean4

@[simp]
theorem mem_mk (c : ℕ × ℕ) (cells) (isLowerSet) : c ∈ YoungDiagram.mk cells isLowerSet ↔ c ∈ cells :=
  Iff.rfl

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

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

Разделы

Аффилиация

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