English
Definition: a reorganized product map that splits a function’s values according to a coordinate set S and its complement.
Русский
Определение: перестановочное отображение произведения, раскладывающее значения функции по координатам в S и в его дополнении.
LaTeX
$$$\text{reorderRestrictProd}: S^c\!\text{.restrict}'' s \times \prod_{i\in S} \alpha_i \to \prod_{i} \alpha_i$$$
Lean4
/-- Given a set in a product space `s : Set (Π j, α j)` and a set of coordinates `S : Set ι`,
`Sᶜ.restrict '' s × (Π i : S, α i)` is the set of functions that coincide with an element of `s`
on `Sᶜ` and are arbitrary on `S`.
`reorderRestrictProd` sends a term of that type to `Π j, α j` by looking for the value at `j`
in one part of the product or the other depending on whether `j` is in `S` or not. -/
noncomputable def reorderRestrictProd (S : Set ι) (s : Set (Π j, α j)) (p : Sᶜ.restrict '' s × (Π i : S, α i)) :
Π j, α j := fun j ↦
if h : j ∈ S then (p.2 : Π j : ↑(S : Set ι), α j) ⟨j, h⟩ else (p.1 : Π j : ↑(Sᶜ : Set ι), α j) ⟨j, h⟩
