get

Mathlib.Data.PFunctor.Multivariate.Basic

URI: https://scilib.ai/kg/mathlib#MvPFunctor.const.get

English

The destructor get simply returns the A-component of a const n A object.

Русский

Деструктор get возвращает A-компонент константного функторa.

LaTeX

$$$$ \\mathrm{const}.get( (a, _) ) = a. $$$$

Lean4

/-- Destructor for the constant functor -/
def get (x : const n A α) : A :=
  x.1

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

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

Разделы

Аффилиация

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