instEpiσ

Mathlib.AlgebraicTopology.SimplexCategory.Basic

URI: https://scilib.ai/kg/mathlib#SimplexCategory.instEpiσ

English

For every n and i in Fin(n+1), the face map σ_i is an epimorphism.

Русский

Для каждого n и i в Fin(n+1) выполняется, что σ_i является эпиморфизмом.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N},\\\\forall i \\\\in \\\\mathrm{Fin}(n+1),\\\\operatorname{Epi}(\\\\sigma_i)$$$

Lean4

instance {n : ℕ} {i : Fin (n + 1)} : Epi (σ i) := by simpa only [epi_iff_surjective] using Fin.predAbove_surjective i

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

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

Разделы

Аффилиация

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