curryFinFinset_symm_apply_const — Mathlib

English

Specializing the symmetric curryFinFinset to a constant input: ((curryFinFinset hk hl).symm f) (const x) = f (const x) (const x).

Русский

Особое значение симметричного каррирования: для константного входа получаем константные аргументы.

LaTeX

$$$((curryFinFinset\\, 𝕜\\ G\\ G' hk hl).symm\\ f\\ fun\\_ => x) = f (fun\\_ => x) (fun\\_ => x).$$$

Lean4

@[simp]
theorem curryFinFinset_symm_apply_const (hk : #s = k) (hl : #sᶜ = l) (f : G [×k]→L[𝕜] G [×l]→L[𝕜] G') (x : G) :
    ((curryFinFinset 𝕜 G G' hk hl).symm f fun _ => x) = f (fun _ => x) fun _ => x :=
  rfl

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