truncate_zero_one — Mathlib

English

Truncating γ from 0 to 1 recovers γ up to the natural cast; i.e., γ.truncate 0 1 is the same as γ.

Русский

Усечение γ по [0,1] восстанавливает γ, т.е. γ.truncate 0 1 совпадает с γ после простой канонической привязки.

LaTeX

$$$ \gamma.truncate(0,1) = \gamma.$$$

Lean4

@[simp]
theorem truncate_zero_one {a b : X} (γ : Path a b) : γ.truncate 0 1 = γ.cast (by simp) (by simp) :=
  by
  ext x
  rw [cast_coe]
  have : ↑x ∈ (Icc 0 1 : Set ℝ) := x.2
  rw [truncate, coe_mk_mk, max_eq_left this.1, min_eq_left this.2, extend_extends']

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