instSetLikeProdNat

Mathlib.Combinatorics.Young.YoungDiagram

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

English

For any c, c ∈ μ.cells iff c ∈ μ (as a point in the plane).

Русский

Для любой пары координат c, c∈μ.cells тогда и только тогда, когда c∈μ.

LaTeX

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

Lean4

instance : SetLike YoungDiagram (ℕ × ℕ) where
  coe y := y.cells
  coe_injective' μ ν h := by rwa [YoungDiagram.ext_iff, ← Finset.coe_inj]

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

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

Разделы

Аффилиация

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