dim_eq_of_mk_eq — Mathlib

English

If two elements x,y of X.S become equal after applying the mk constructor, then their dimensions are equal: dim(x) = dim(y).

Русский

Если две части X.S, x и y, становятся равными после применения конструктора mk, тогда их размерности совпадают: dim(x) = dim(y).

LaTeX

$$$\forall x,y:\ X.S,\ (\mathrm{mk}(x) = \mathrm{mk}(y)) \Rightarrow x.dim = y.dim$$$

Lean4

theorem dim_eq_of_mk_eq {n m : ℕ} {x : X _⦋n⦌} {y : X _⦋m⦌} (h : S.mk x = S.mk y) : n = m :=
  dim_eq_of_eq h

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