funSplitAt — Mathlib

English

For a fixed index i, the function type α → β is equivalent to β × ({ j | j ≠ i } → β).

Русский

Для фиксированного индекса i функция α → β эквивалентна β × ({ j | j ≠ i } → β).

LaTeX

$$$\text{Equiv}(\alpha \to \beta) \cong \beta \times (\{ j \mid j \neq i \} \to \beta).$$$

Lean4

/-- A product of copies of a type can be split as the binary product of one copy and the product
  of all the remaining copies. -/
@[simps!]
def funSplitAt {α : Type*} [DecidableEq α] (i : α) (β : Type*) : (α → β) ≃ β × ({ j // j ≠ i } → β) :=
  piSplitAt i _

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