cast_eq_self

Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

URI: https://scilib.ai/kg/mathlib#SSet.N.cast_eq_self

English

If s.dim = d, then casting s along hd yields s again; cast is idempotent on the dimension-equal instance.

Русский

Если dim(s) = d, то cast hd возвращает s; cast не меняет элемент при совпадении размерности.

LaTeX

$$$ cast_eq_self : \forall {X} (s:\ X.N) {d : Nat} (hd : s.dim = d), s.cast hd = s$$$

Lean4

theorem cast_eq_self : s.cast hd = s := by
  subst hd
  rfl

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

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

Разделы

Аффилиация

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