to_fun_eq_coe — Mathlib

English

For any μ and tableau T, the entry function equals the coe of T, i.e. T.entry equals the function T seen as ℕ → ℕ → ℕ.

Русский

Для любой пары μ и табло T функция записи равна отображению T как функции, т. е. T.entry = (T : ℕ → ℕ → ℕ).

LaTeX

$$$T.\mathrm{entry} = (T: \mathbb{N} \to \mathbb{N} \to \mathbb{N}).$$$

Lean4

@[simp]
theorem to_fun_eq_coe {μ : YoungDiagram} {T : SemistandardYoungTableau μ} : T.entry = (T : ℕ → ℕ → ℕ) :=
  rfl

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