cast_eq_self — Mathlib

English

Let s be a simplex in a simplicial set X with dimension d. Then the cast of s along the equality hd: s.dim = d is equal to s itself.

Русский

Пусть s — симплекс в симплициальном множестве X с размерностью d. Тогда приведение s по равенству hd: s.dim = d даст то же самое s.

LaTeX

$$$s.cast(hd) = s$$$

Lean4

theorem cast_eq_self : s.cast hd = s := by
  obtain ⟨d, _, rfl⟩ := s.mk_surjective
  obtain rfl := hd
  rfl

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