default_consistent — Mathlib

English

A variant of the previous result: for x : (n ↦ CofixA F n) with AllAgree, the heads at height n+1 are equal for all n and m.

Русский

Вариант предыдущего результата: для x: (n ↦ CofixA F n) с AllAgree головы на высоте n+1 совпадают для любых n и m.

LaTeX

$$$\\forall F,\\forall n,m:\\mathbb{N},\\forall x:\\, (n\\mapsto \\operatorname{CofixA} F n),\\; \\operatorname{AllAgree} x \\;\\to\\; \\operatorname{head}'(x(\\operatorname{succ} n)) = \\operatorname{head}'(x(\\operatorname{succ} m)).$$$

Lean4

theorem default_consistent [Inhabited F.A] : ∀ n, Agree (default : CofixA F n) default
  | 0 => Agree.continu _ _
  | succ n => Agree.intro _ _ fun _ => M.default_consistent n

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