snoc_castSucc — Mathlib

English

instLTNat.lt a.val n is True; i.e., the standard less-than predicate for a Fin element holds in its natural bound.

Русский

instLTNat.lt a.val n истинно; то есть стандартное неравенство меньше используется для элемента Fin.

LaTeX

$$$\\operatorname{instLTNat}.lt\\ (a.\\text{val})\\ n = \\text{True}$$$

Lean4

@[simp]
theorem snoc_castSucc : snoc p x i.castSucc = p i :=
  by
  simp only [snoc, coe_castSucc, is_lt, cast_eq, dite_true]
  convert cast_eq rfl (p i)

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