head'_eq_head

Mathlib.Data.PFunctor.Univariate.M

URI: https://scilib.ai/kg/mathlib#PFunctor.M.head'_eq_head

English

Equivalently, for any x ∈ M F and n, head'(x.approx (n+1)) equals head x.

Русский

Эквивалентно: head'(x.approx (n+1)) равно head x.

LaTeX

$$$\\forall F,\\forall x:\\, M F,\\; \\operatorname{head}'(x.approx (n+1)) = \\operatorname{head} x.$$$

Lean4

theorem head'_eq_head : ∀ (x : M F) (n : ℕ), head' (x.approx <| n + 1) = head x
  | ⟨_, h⟩, _ => head_succ' _ _ _ h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru