finSigmaFinEquiv_apply — Mathlib

English

For k = (i, j) in (Fin m) × Fin (n i), the index under the bijection is the sum of the preceding n-values plus j; equivalently, the image is the obvious flattened index.

Русский

Для k = (i, j) в (Fin m) × Fin (n i) образ под биекцией равен сумме предыдущих значений n до i плюс j; иначе говоря, образ — это естественный «плоский» индекс.

LaTeX

$$$\\text{Let } k=(i,j)\\in (\\mathrm{Fin} m)\\times \\mathrm{Fin}(n\\,i).\\quad\n\\mathrm{finSigmaFinEquiv}(k) = \\left(\\sum_{t:\\mathrm{Fin} m, t

Lean4

@[simp]
theorem finSigmaFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) :
    (finSigmaFinEquiv k : ℕ) = ∑ i : Fin k.1, n (Fin.castLE k.1.2.le i) + k.2 := by
  induction m with
  | zero => exact k.fst.elim0
  | succ m ih =>
    rcases k with ⟨⟨iv, hi⟩, j⟩
    rw [finSigmaFinEquiv]
    unfold finSumFinEquiv
    simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.trans_def, Equiv.trans_apply,
      finCongr_apply, Fin.coe_cast]
    by_cases him : iv < m
    · conv in Sigma.mk _ _ => equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]
      simpa using ih _
    · replace him := Nat.eq_of_lt_succ_of_not_lt hi him
      subst him
      conv in Sigma.mk _ _ => equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]
      simp
      rfl

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