subtypeVal_nil — Mathlib

English

Let α be a 0-length TypeVec and ps be a family of propositions indexed by α. Then the subtype-valued map equals the nil function.

Русский

Пусть α — вектор типов нулевой длины, и ps — семейство пропозиций, индексируемое α. Тогда отображение subtypeVal является пустой функцией.

LaTeX

$$$(|\alpha|=0) \Rightarrow \operatorname{subtypeVal}(ps) = \operatorname{nilFun}$$$

Lean4

theorem subtypeVal_nil {α : TypeVec.{u} 0} (ps : α ⟹ «repeat» 0 Prop) : TypeVec.subtypeVal ps = nilFun :=
  funext <| by rintro ⟨⟩

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