cast_segment — Mathlib

English

If c = a and d = b, then casting the segment from a to b yields the segment from c to d; endpoints are preserved under equality substitutions.

Русский

Если c = a и d = b, то приведение сегмента от a к b к сегменту от c к d сохраняет концы.

LaTeX

$$$ (Path.segment\ a\ b).cast (hac) (hbd) = Path.segment\ c\ d \text{ whenever } c=a\text{ and } d=b $$$

Lean4

@[simp]
theorem cast_segment {a b c d : E} (hac : c = a) (hbd : d = b) : (Path.segment a b).cast hac hbd = .segment c d := by
  subst_vars; rfl

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