map_le_succ

Mathlib.CategoryTheory.Functor.OfSequence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.OfSequence.map_le_succ

← MathLib Explorer

English

The right-ward map along i to i+1 equals f_i when taking i to i+1.

Русский

Перемещение вправо вдоль i до i+1 эквивалентно f_i при задании i.

LaTeX

$$$\\forall i,\\ map f i (i+1) (by cutsat) = f_i.$$$

Lean4

theorem map_le_succ (i : ℕ) : map f i (i + 1) (by cutsat) = f i :=
  by
  revert X f
  induction i with
  | zero => intros; rfl
  | succ _ hi =>
    intro X f
    apply hi

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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