map_finCongr_Ici — Mathlib

English

Let h : n = m and i ∈ Fin n. The image of Ici(i) under Fin.cast h is Ici(i.cast h).

Русский

Пусть h : n = m и i ∈ Fin n. Образ Ici(i) при приведении Fin.cast h равен Ici(i.cast h).

LaTeX

$$$$ \operatorname{Finset.image}(\operatorname{Fin.cast} h)(\operatorname{Finset.Ici}(i)) = \operatorname{Finset.Ici}(\operatorname{Fin.cast} h\, i) $$$$

Lean4

@[simp]
theorem map_finCongr_Ici (h : n = m) (i : Fin n) : (Ici i).map (finCongr h).toEmbedding = Ici (i.cast h) := by
  simp [← coe_inj]

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