reindex_apply — Mathlib

English

Applying reindex to a ray yields the corresponding reindexed ray under domDomCongr.

Русский

Применение повторной индексации к лучу дает соответствующий переиндексированный луч.

LaTeX

$$$\text{reindex_apply}: (e) \;:\; Orientation.reindex R M e (rayOfNeZero _ v hv) = rayOfNeZero _ (v.domDomCongr e) (mt (v.domDomCongr_eq_zero_iff e).mp hv).$$$

Lean4

@[simp]
theorem reindex_apply (e : ι ≃ ι') (v : M [⋀^ι]→ₗ[R] R) (hv : v ≠ 0) :
    Orientation.reindex R M e (rayOfNeZero _ v hv) =
      rayOfNeZero _ (v.domDomCongr e) (mt (v.domDomCongr_eq_zero_iff e).mp hv) :=
  rfl

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