_aux_Mathlib_AlgebraicTopology_SimplicialSet_Boundary___delab_app_Simplicial_term∂Δ[_]_1

Mathlib.AlgebraicTopology.SimplicialSet.Boundary

URI: https://scilib.ai/kg/mathlib#Simplicial._aux_Mathlib_AlgebraicTopology_SimplicialSet_Boundary___delab_app_Simplicial_term∂Δ[_]_1

← MathLib Explorer

Lean4

/-- Pretty printer defined by `notation3` command. -/
@[scoped delab✝ app.SSet.boundary]
public meta def «_aux_Mathlib_AlgebraicTopology_SimplicialSet_Boundary___delab_app_Simplicial_term∂Δ[_]_1» : Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 1
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `SSet.boundary)) (matchVar✝ `n) >=> pure✝) MatchState.empty✝ >>=
            fun s✝ => MatchState.delabVar✝ s✝ `n (some✝ e✝) >>= fun n => withHeadRefIfTagAppFns✝ `(∂Δ[$n]))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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