mem_cylinder_firstDiff

Mathlib.Topology.MetricSpace.PiNat

URI: https://scilib.ai/kg/mathlib#PiNat.mem_cylinder_firstDiff

English

For x,y, x ∈ cylinder y (firstDiff x y).

Русский

Для последовательностей x,y: x принадлежит цилиндру вокруг y на позиции firstDiff x y.

LaTeX

$$$x \\in \\mathrm{cylinder}(y,\\mathrm{firstDiff}(x,y))$$$

Lean4

theorem mem_cylinder_firstDiff (x y : ∀ n, E n) : x ∈ cylinder y (firstDiff x y) := fun _i hi =>
  apply_eq_of_lt_firstDiff hi

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

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

Разделы

Аффилиация

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