English
Let E be an equivalence-like relation between index sets ι' and ι. For any v1: ι → P1 and v2: ι → P2, v1 ∘ f ≅ v2 ∘ f if and only if v1 ≅ v2, where f: E describes the equivalence.
Русский
Пусть E описывает эквиваленцию между множестами индексов ι' и ι. Тогда для любых v1: ι → P1, v2: ι → P2, v1 ∘ f ≅ v2 ∘ f эквивалентно v1 ≅ v2, где f задаёт эквиваленцию.
LaTeX
$$$ (v_1 \circ f) \cong v_2 \circ f \;\;\text{iff}\;\; v_1 \cong v_2 $$$
Lean4
/-- Change between equivalent index sets ι and ι'. -/
@[simp]
theorem index_equiv {E : Type*} [EquivLike E ι' ι] (f : E) (v₁ : ι → P₁) (v₂ : ι → P₂) : v₁ ∘ f ≅ v₂ ∘ f ↔ v₁ ≅ v₂ :=
by
refine ⟨fun h i₁ i₂ ↦ ?_, fun h ↦ index_map h f⟩
simpa [(EquivLike.toEquiv f).right_inv i₁, (EquivLike.toEquiv f).right_inv i₂] using
edist_eq h ((EquivLike.toEquiv f).symm i₁) ((EquivLike.toEquiv f).symm i₂)
