English
Given a tableau T, an entry function entry' and a proof h that entry' equals T, T.copy entry' h is a tableau with entry' as its entry and the same row/column structure as T.
Русский
Для тaбло T, функции записи entry' и доказательства h, что entry'=T, копия T.copy entry' h имеет entry' как запись и ту же структуру.
LaTeX
$$$\forall \mu:\; T: \mathrm{SemistandardYoungTableau}(\mu),\; entry': \mathbb{N}\to\mathbb{N}\to\mathbb{N},\; h: entry' = T\;:\; T.copy(entry')(h) : \mathrm{SemistandardYoungTableau}(\mu).$$$
Lean4
/-- Copy of an `SemistandardYoungTableau μ` with a new `entry` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (entry' : ℕ → ℕ → ℕ) (h : entry' = T) :
SemistandardYoungTableau μ where
entry := entry'
row_weak' := h.symm ▸ T.row_weak'
col_strict' := h.symm ▸ T.col_strict'
zeros' := h.symm ▸ T.zeros'
