instFunLike — Mathlib

English

There is a FunLike structure on SemistandardYoungTableau μ in the evident way, aligning the coe with the entry function.

Русский

Существует структура FunLike на SemistandardYoungTableau μ в явном виде, соответствующая отображению коe таблицы значению элемента.

LaTeX

$$$\exists f: \mathrm{SemistandardYoungTableau}(\mu) \to (\mathbb{N} \to \mathbb{N}),\; f = \mathrm{entry}.$$$

Lean4

instance instFunLike {μ : YoungDiagram} : FunLike (SemistandardYoungTableau μ) ℕ (ℕ → ℕ)
    where
  coe := SemistandardYoungTableau.entry
  coe_injective' T T'
    h := by
    cases T
    cases T'
    congr

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