ofLine_extend — Mathlib

English

If we take Path.ofLine with endpoints coming from γ, we recover γ.

Русский

Если взять Path.ofLine с концами, полученными из γ, то восстанавливается сам γ.

LaTeX

$$$\mathrm{Path.ofLine}(\text{hf}, \mathrm{extend\_zero}(\gamma), \mathrm{extend\_one}(\gamma)) = \gamma$$$

Lean4

@[simp]
theorem ofLine_extend (γ : Path x y) : ofLine (by fun_prop) (extend_zero γ) (extend_one γ) = γ :=
  by
  ext t
  simp [ofLine]

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