extendMap_id_f — Mathlib

English

The f-component of extendMap of the identity is the identity on the extended X, i.e., (extendMap (id K) e).f i' = id.

Русский

Компонента f для extendMap от единицы равна единице на расширенной X.

LaTeX

$$$(\\text{extendMap} (\\mathrm{id} K) e).f i' = \\mathrm{id}$$$

Lean4

theorem extendMap_id_f (i' : ι') : (extendMap (𝟙 K) e).f i' = 𝟙 _ :=
  by
  by_cases hi' : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hi'
    simp [extendMap_f _ e hi]
  · apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

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