mk

Mathlib.ModelTheory.DirectLimit

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Structure.Sigma.mk

English

There is a constructor that builds an element of the dependent sum by pairing an index i with an element x ∈ G_i.

Русский

Существуют конструктор, который составит пару (i, x) из индекса i и элемента x ∈ G_i.

LaTeX

$$$\\mathrm{mk}_f(i,x)\\in \\Sigma f$$$

Lean4

/-- Constructor for `FirstOrder.Language.Structure.Sigma` alias. -/
abbrev mk (i : ι) (x : G i) : Σˣ f :=
  ⟨i, x⟩

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

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

Разделы

Аффилиация

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