degenerate_app_apply — Mathlib

English

If x is a degenerate n-simplex of X and f: X → Y is a simplicial map, then f(x) is a degenerate n-simplex of Y.

Русский

Пусть x — вырожденная n-ъ-грань в X, а f: X → Y — отображение. Тогда f(x) — вырожденная n-грань в Y.

LaTeX

$$$$x \in X_{\mathrm{deg}}(n) \implies f(x) \in Y_{\mathrm{deg}}(n),$$$$

Lean4

theorem degenerate_app_apply {n : ℕ} {x : X _⦋n⦌} (hx : x ∈ X.degenerate n) (f : X ⟶ Y) : f.app _ x ∈ Y.degenerate n :=
  by
  obtain ⟨m, hm, g, y, rfl⟩ := hx
  exact ⟨m, hm, g, f.app _ y, by rw [FunctorToTypes.naturality]⟩

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