index_extendMiddle_zero — Mathlib

English

The index of 0 in the extended partition equals i: (c.extendMiddle i).index 0 = i.

Русский

Индекс нуля в расширенном разбиении равен i: (c.extendMiddle i).index 0 = i.

LaTeX

$$$ (\\mathrm{extendMiddle}\\, i).\\mathrm{index}\\,0 = i $$$

Lean4

theorem index_extendMiddle_zero (c : OrderedFinpartition n) (i : Fin c.length) : (c.extendMiddle i).index 0 = i :=
  by
  have : (c.extendMiddle i).emb i 0 = 0 := by simp [extendMiddle]
  conv_rhs at this => rw [← (c.extendMiddle i).emb_invEmbedding 0]
  contrapose! this
  exact (c.extendMiddle i).emb_ne_emb_of_ne (Ne.symm this)

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