component

Mathlib.Topology.Category.LightProfinite.AsLimit

URI: https://scilib.ai/kg/mathlib#LightProfinite.component

English

An abbreviation for the nth component of S.diagram, i.e., component(n) = S.diagram.obj ⟨n⟩.

Русский

Сокращение для n-й компоненты диаграммы S: component(n) = S.diagram.obj ⟨n⟩.

LaTeX

$$$\\text{component}(n) := S.diagram.obj\\langle n \\rangle$$$

Lean4

/-- An abbreviation for the `n`th component of `S.diagram`. -/
abbrev component (n : ℕ) : LightProfinite :=
  S.diagram.obj ⟨n⟩

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

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

Разделы

Аффилиация

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