cast_top — Mathlib

English

If m = n, then the top element is preserved under cast: (⊤ : Fin m).cast h = ⊤ for h : m = n.

Русский

Если m = n, то верхний элемент сохраняется под приведением: (⊤ : Fin m).cast h = ⊤ для h : m = n.

LaTeX

$$$\forall {m,n} (h : m = n), (\top : \mathrm{Fin}(m)).\mathrm{cast} h = \top$$$

Lean4

@[simp]
theorem cast_top {m n : ℕ} [NeZero m] [NeZero n] (h : m = n) : (⊤ : Fin m).cast h = ⊤ := by simp [← val_inj, h]

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