map_finCongr_Icc — Mathlib

English

Let h : n = m and i,j ∈ Fin n. The image of Icc(i,j) under the embedding given by finCongr h is Icc(i.cast h, j.cast h).

Русский

Пусть h : n = m и i, j ∈ Fin n. Образ Icc(i,j) под отображением, порождаемым finCongr h, равен Icc(i.cast h, j.cast h).

LaTeX

$$$$ (\operatorname{Finset.Icc}(i, j)).map (\operatorname{finCongr} h).toEmbedding = \operatorname{Finset.Icc}(\operatorname{Fin.cast} h\, i, \operatorname{Fin.cast} h\, j) $$$$

Lean4

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

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