curryFinFinset_symm_apply_piecewise_const

English

Describes the full symmetry of the curryFinFinset isomorphism in terms of coordinates.

Русский

Определение полной симметрии изоморфизма curryFinFinset относительно координат.

LaTeX

$$$ (curryFinFinset R M_2 M' hk hl).symm f\\; m = \\; f(\\lambda i. m<|inl i|) (\\lambda i'. m<|inr i'|) $$$

Lean4

theorem curryFinFinset_symm_apply_piecewise_const {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l)
    (f : MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂)) (x y : M') :
    (curryFinFinset R M₂ M' hk hl).symm f (s.piecewise (fun _ => x) fun _ => y) = f (fun _ => x) fun _ => y :=
  by
  rw [curryFinFinset_symm_apply]; congr
  · ext
    rw [finSumEquivOfFinset_inl, Finset.piecewise_eq_of_mem]
    apply Finset.orderEmbOfFin_mem
  · ext
    rw [finSumEquivOfFinset_inr, Finset.piecewise_eq_of_notMem]
    exact Finset.mem_compl.1 (Finset.orderEmbOfFin_mem _ _ _)

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