dropFun_subtypeVal — Mathlib

English

Dropping the functor from subtypeVal yields the same as applying subtypeVal to a placeholder.

Русский

Уменьшая размерность через dropFun к subtypeVal, получаем subtypeVal от некого аргумента.

LaTeX

$$\operatorname{dropFun}(\operatorname{subtypeVal}(p)) = \operatorname{subtypeVal}(\_)$$

Lean4

@[simp]
theorem dropFun_subtypeVal {α} (p : α ⟹ «repeat» (n + 1) Prop) : dropFun (subtypeVal p) = subtypeVal _ :=
  rfl

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