ext — Mathlib

English

If two SemistandardYoungTableau μ agree on all entries, they are equal.

Русский

Если два SemistandardYoungTableau μ совпадают во всех клетках, они равны.

LaTeX

$$$\forall T,T': \ SemistandardYoungTableau(\mu),\ (\forall i,j: T(i,j)=T'(i,j)) \Rightarrow T=T'.$$$

Lean4

@[ext]
theorem ext {μ : YoungDiagram} {T T' : SemistandardYoungTableau μ} (h : ∀ i j, T i j = T' i j) : T = T' :=
  DFunLike.ext T T' fun _ ↦ by
    funext
    apply h

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