truncate_one_one — Mathlib

English

For any γ and t, truncating at t,t is the same as the extended path at t, up to the canonical cast.

Русский

Для любой γ и любого t усечение γ по t и t совпадает с расширением γ по t при каноническом отображении.

LaTeX

$$$ \gamma.truncate(0,0) = (\mathrm{Path.refl}(\gamma.extend(0))).cast(\text{by } \min_self)\, \gamma.extend(0). $$$

Lean4

theorem truncate_one_one {a b : X} (γ : Path a b) :
    γ.truncate 1 1 = (Path.refl b).cast (by rw [min_self, γ.extend_one]) γ.extend_one := by convert γ.truncate_self 1

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