head_succ — Mathlib

English

For any F and x : M F, the head of x at height succ n is independent of n and m; head'(x.approx (succ n)) = head'(x.approx (succ m)).

Русский

Для любого F и x ∈ M F голова x на высоте succ n не зависит от n и m; head'(x.approx (succ n)) = head'(x.approx (succ m)).

LaTeX

$$$\\forall F, \\forall n,m:\\mathbb{N}, \\forall x:\\, M F,\\; \\operatorname{head}'(x.approx(\\operatorname{succ} n)) = \\operatorname{head}'(x.approx(\\operatorname{succ} m)).$$$

Lean4

theorem head_succ (n m : ℕ) (x : M F) : head' (x.approx (succ n)) = head' (x.approx (succ m)) :=
  head_succ' n m _ x.consistent

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