boundary_ι_mem_I — Mathlib

English

For every n, the boundary inclusion ι: ∂Δ[n] → Δ[n] lies in the distinguished class I of morphisms (i.e., is included as an admissible map in the framework).

Русский

Для каждого n граница ∂Δ[n] → Δ[n] принадлежит особому классу I морфизмов (то есть является допустимым отображением в рамках структуры).

LaTeX

$$$ \\iota: \\partial \\Delta[n] \\hookrightarrow \\Delta[n] \\in I$$$

Lean4

theorem boundary_ι_mem_I (n : ℕ) : I (boundary.{u} n).ι := by constructor

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