vectorAllP_singleton

Mathlib.Data.Vector3

URI: https://scilib.ai/kg/mathlib#vectorAllP_singleton

English

For any p and x, VectorAllP p (cons x []) equals p x, i.e., the single coordinate satisfies p.

Русский

Для любого p и x, VectorAllP p (cons x []) равно p x, то есть единственный координат удовлетворяет p.

LaTeX

$$$\mathrm{VectorAllP}(p,\mathrm{cons}(x,\,\mathrm{Vector3.nil})) = p(x).$$$

Lean4

@[simp]
theorem vectorAllP_singleton (p : α → Prop) (x : α) : VectorAllP p (cons x []) = p x :=
  rfl

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

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

Разделы

Аффилиация

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