consPiProd — Mathlib

English

Split the Pi-type over a cons into a pair consisting of the value at a and the Pi-type over the rest.

Русский

Разделить зависимую произведение по индексу a и остаток; получить пару: значение в a и зависимое произведение по оставшимся индексам.

LaTeX

$$$\text{consPiProd} : (\Pi i \in \operatorname{cons}(a,s\,has), f\,i) \cong f(a) \times (\Pi i \in s, f(i))$$$

Lean4

/-- Split the added element of cons off a Pi type. -/
@[simps!]
def consPiProd (f : α → Type*) (has : a ∉ s) (x : Π i ∈ cons a s has, f i) : f a × Π i ∈ s, f i :=
  (x a (mem_cons_self a s), fun i hi => x i (mem_cons_of_mem hi))

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