index_map — Mathlib

English

Let v1: ι → P1 and v2: ι → P2 be congruent, i.e. the pairwise extended distances between their values agree. For any map f: ι' → ι, the pulled-back families v1 ∘ f and v2 ∘ f are also congruent.

Русский

Пусть v1: ι → P1 и v2: ι → P2 согласованы, то есть расстояния между их значениями сохраняются. Для любой отображения f: ι' → ι композиция v1 ∘ f и v2 ∘ f также согласованы.

LaTeX

$$$ (v_1 \circ f) \cong (v_2 \circ f) $$$

Lean4

/-- Change the index set ι to an index ι' that maps to ι. -/
theorem index_map (h : v₁ ≅ v₂) (f : ι' → ι) : (v₁ ∘ f) ≅ (v₂ ∘ f) := fun i₁ i₂ ↦ edist_eq h (f i₁) (f i₂)

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