range_eq_ofSimplex

Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

URI: https://scilib.ai/kg/mathlib#SSet.Subcomplex.range_eq_ofSimplex

English

If f: Δ[n] ⟶ X, then the range Subpresheaf of f equals Subcomplex.ofSimplex of yonedaEquiv f.

Русский

Если f: Δ[n] ⟶ X, то образ f как подпредпосылается равен Subcomplex.ofSimplex(yonedaEquiv f).

LaTeX

$$Subpresheaf.range f = ofSimplex (yonedaEquiv f)$$

Lean4

theorem range_eq_ofSimplex {n : ℕ} (f : Δ[n] ⟶ X) : Subpresheaf.range f = ofSimplex (yonedaEquiv f) :=
  Subpresheaf.range_eq_ofSection' _

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

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

Разделы

Аффилиация

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