finPiFinEquiv — Mathlib

English

Equivalence between the type of functions from Fin m to Fin n and Fin (∏ i: Fin m, n i); this is a higher-arity generalization of the previous equivalence.

Русский

Эквиваленция между типом функций из Fin m в Fin n и Fin (∏ i: Fin m, n i).

LaTeX

$$$$ (\\mathrm{finPiFinEquiv}) : (\\forall i: \\mathrm{Fin} m, \\mathrm{Fin}(n i)) \\simeq \\mathrm{Fin}\\left(\\prod_{i: \\mathrm{Fin} m} n i\\right).$$$$

Lean4

/-- Equivalence between `∀ i : Fin m, Fin (n i)` and `Fin (∏ i : Fin m, n i)`. -/
def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃ Fin (∏ i : Fin m, n i) :=
  Equiv.ofRightInverseOfCardLE (le_of_eq <| by simp_rw [Fintype.card_pi, Fintype.card_fin])
    (fun f =>
      ⟨∑ i, f i * ∏ j, n (Fin.castLE i.is_lt.le j), by
        induction m with
        | zero => simp
        | succ m ih =>
          rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
          suffices
            ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
              ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
                (∏ i : Fin m, n i) * nn
            by solve_by_elim
          intro n nn f fn
          cases nn
          · exact isEmptyElim fn
          refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_
          rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]⟩)
    (fun a b =>
      ⟨(a / ∏ j : Fin b, n (Fin.castLE b.is_lt.le j)) % n b,
        by
        cases m
        · exact b.elim0
        rcases h : n b with nb | nb
        · rw [prod_eq_zero (Finset.mem_univ _) h] at a
          exact isEmptyElim a
        exact Nat.mod_lt _ nb.succ_pos⟩)
    (by
      intro a; revert a; dsimp only [Fin.val_mk]
      refine Fin.consInduction ?_ ?_ n
      · intro a
        have : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) := (finCongr <| prod_empty).subsingleton
        subsingleton
      · intro n x xs ih a
        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
        ext
        simp_rw [Fin.sum_univ_succ, Fin.cons_succ]
        have := fun i : Fin n =>
          Fintype.prod_equiv (finCongr <| Fin.val_succ i)
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Nat.succ_le_succ (Fin.is_lt _).le) j)) fun j => rfl
        simp_rw [this]
        clear this
        simp_rw [Fin.val_zero, Fintype.prod_empty, Nat.div_one, mul_one, Fin.cons_zero, Fin.prod_univ_succ,
          Fin.castLE_zero, Fin.cons_zero, ← Nat.div_div_eq_div_mul, mul_left_comm (_ % _ : ℕ), ← mul_sum]
        convert Nat.mod_add_div _ _
        exact ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq (Fin.prod_univ_succ _)))

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