extendMap_f_eq_zero — Mathlib

English

The f-component of the extended map is zero at i' whenever the embedding misses i'.

Русский

Компонента f расширенной карты равна нулю на i', если вложение e не достигло какого-либо i.

LaTeX

$$$(extendMap\\; \\phi\\; e).f i' = 0$ when the image misses i'$$

Lean4

theorem extendMap_f_eq_zero (i' : ι') (hi' : ∀ i, e.f i ≠ i') : (extendMap φ e).f i' = 0 :=
  by
  dsimp [extendMap]
  rw [extend.mapX_none φ (e.r_eq_none i' hi')]

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