truncate_zero_zero — Mathlib

English

For any path γ and any t, truncating at 1,1 yields the extended path at the end point, i.e., γ.truncate 1 1 equals the extension at the endpoint b, up to the canonical cast.

Русский

Для траектории γ усечение по 1 и 1 даёт путь, совпадающий с продолжением на конечной точке, то есть γ.truncate 1 1 идентично γ.extend 1 (считая каноническое отображение).

LaTeX

$$$ \gamma.truncate(1,1) = \big( \mathrm{Path.refl}(\gamma.extend(1)) \big).cast(\ldots) \ gamma.extend(1). $$$

Lean4

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

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