rightExtensionInclusion — Mathlib

English

The order-embedded J is less-than or equal to the monomorphisms; every element of J is mono.

Русский

Порядковая вложенность J по отношению к монообразам: каждый элемент J является монообразом.

LaTeX

$$$ J \\leq \\mathrm{monomorphisms}$$$

Lean4

/-- The identity natural transformation exhibits a simplicial set as a right extension of its
restriction along `(Truncated.inclusion (n := n)).op`. -/
@[simps!]
def rightExtensionInclusion (X : SSet.{u}) (n : ℕ) :
    RightExtension (Truncated.inclusion (n := n)).op ((Truncated.inclusion n).op ⋙ X) :=
  RightExtension.mk _ (𝟙 _)

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