sigmaCurry_smul — Mathlib

English

Curry of a single coordinate under sigma-curry yields a nested single: sigmaCurry (single ij x) = single ij.fst (single ij.snd x).

Русский

Складывание одного координатного элемента через σ-куррирование даёт вложенный одинарный элемент: sigmaCurry (single (i,j) x) = single i (single j x).

LaTeX

$$$\sigma\text{-Curry}(\text{single } (i,j) x) = \text{single } i (\text{single } j x)$$$

Lean4

@[simp]
theorem sigmaCurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)] (r : γ)
    (f : Π₀ (i : Σ _, _), δ i.1 i.2) : sigmaCurry (r • f) = (r • sigmaCurry f : Π₀ (i) (j), δ i j) :=
  by
  ext (i j)
  rfl

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